lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2).
#T1 #T2 #f1 #H elim H -T1 -T2 -f1
/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/
lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≘ T2).
#T1 #T2 #f1 #H elim H -T1 -T2 -f1
/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/