#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
qed-.
lemma liftsb_refl: ∀f. 𝐈⦃f⦄ → reflexive … (liftsb f).
/3 width=1 by lifts_refl, ext2_refl/ qed.
#I1 #I2 #f1 * -I1 -I2 /3 width=3 by lifts_eq_repl_back, ext2_pair/
qed-.
lemma liftsb_refl: ∀f. 𝐈⦃f⦄ → reflexive … (liftsb f).
/3 width=1 by lifts_refl, ext2_refl/ qed.