#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
qed-.
-lemma liftsb_refl: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 → reflexive … (liftsb f).
+lemma liftsb_refl: â\88\80f. ð\9d\90\88â\9dªfâ\9d« → reflexive … (liftsb f).
/3 width=1 by lifts_refl, ext2_refl/ qed.
lemma liftsb_total: ∀I1,f. ∃I2. ⇧*[f] I1 ≘ I2.
(* Basic forward lemmas *****************************************************)
-lemma liftsb_fwd_isid: â\88\80f,I1,I2. â\87§*[f] I1 â\89\98 I2 â\86\92 ð\9d\90\88â¦\83fâ¦\84 → I1 = I2.
+lemma liftsb_fwd_isid: â\88\80f,I1,I2. â\87§*[f] I1 â\89\98 I2 â\86\92 ð\9d\90\88â\9dªfâ\9d« → I1 = I2.
#f #I1 #I2 * -I1 -I2 /3 width=3 by lifts_fwd_isid, eq_f2/
qed-.