+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/
+qed-.
+
+lemma lifts_eq_repl_fwd: ∀T1,T2. eq_repl_fwd … (λf. ⬆*[f] T1 ≘ T2).
+#T1 #T2 @eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *)
+qed-.
+
+(* Basic_1: includes: lift_r *)
+(* Basic_2A1: includes: lift_refl *)
+lemma lifts_refl: ∀T,f. 𝐈⦃f⦄ → ⬆*[f] T ≘ T.
+#T elim T -T *
+/4 width=3 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/
+qed.
+
+(* Basic_2A1: includes: lift_total *)
+lemma lifts_total: ∀T1,f. ∃T2. ⬆*[f] T1 ≘ T2.
+#T1 elim T1 -T1 *
+/3 width=2 by lifts_lref, lifts_sort, lifts_gref, ex_intro/
+[ #p ] #I #V1 #T1 #IHV1 #IHT1 #f
+elim (IHV1 f) -IHV1 #V2 #HV12
+[ elim (IHT1 (⫯f)) -IHT1 /3 width=2 by lifts_bind, ex_intro/
+| elim (IHT1 f) -IHT1 /3 width=2 by lifts_flat, ex_intro/
+]
+qed-.
+
+lemma lift_lref_uni: ∀l,i. ⬆*[l] #i ≘ #(l+i).
+#l elim l -l /2 width=1 by lifts_lref/
+qed.
+