-lemma sfr_abbr: â\88\80L,V,e. â\89¼ [0, e] L â\86\92 â\89¼ [0, e + 1] L.ⓓV.
+lemma sfr_abbr: â\88\80L,V,e. â\89½ [0, e] L â\86\92 â\89½ [0, e + 1] L.ⓓV.
-lemma sfr_skip: â\88\80I,L,V,d,e. â\89¼ [d, e] L â\86\92 â\89¼ [d + 1, e] L.ⓑ{I}V.
+lemma sfr_skip: â\88\80I,L,V,d,e. â\89½ [d, e] L â\86\92 â\89½ [d + 1, e] L.ⓑ{I}V.
lapply (HL … HLX) -HL -HLX /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
lapply (HL … HLX) -HL -HLX /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
-lemma sfr_inv_bind: â\88\80I,L,V,e. â\89¼ [0, e] L.ⓑ{I}V → 0 < e →
- â\89¼ [0, e - 1] L ∧ I = Abbr.
+lemma sfr_inv_bind: â\88\80I,L,V,e. â\89½ [0, e] L.ⓑ{I}V → 0 < e →
+ â\89½ [0, e - 1] L ∧ I = Abbr.
-lemma sfr_inv_skip: â\88\80I,L,V,d,e. â\89¼ [d, e] L.â\93\91{I}V â\86\92 0 < d â\86\92 â\89¼ [d - 1, e] L.
+lemma sfr_inv_skip: â\88\80I,L,V,d,e. â\89½ [d, e] L.â\93\91{I}V â\86\92 0 < d â\86\92 â\89½ [d - 1, e] L.