-(* Basic_2A1: includes: lift_inj *)
-theorem lifts_inj: ∀t,T1,U. ⬆*[t] T1 ≡ U → ∀T2. ⬆*[t] T2 ≡ U → T1 = T2.
-#t #T1 #U #H elim H -t -T1 -U
-[ /2 width=2 by lifts_inv_sort2/
-| #i1 #j #t #Hi1j #X #HX elim (lifts_inv_lref2 … HX) -HX
- /4 width=4 by at_inj, eq_f/
-| /2 width=2 by lifts_inv_gref2/
-| #a #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_bind2 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
-| #I #V1 #V2 #T1 #T2 #t #_ #_ #IHV12 #IHT12 #X #HX elim (lifts_inv_flat2 … HX) -HX
- #V #T #HV1 #HT1 #HX destruct /3 width=1 by eq_f2/
+(* Basic_1: includes: lift_gen_lift *)
+(* Basic_2A1: includes: lift_div_le lift_div_be *)
+theorem lifts_div4: ∀f2,Tf,T. ⬆*[f2] Tf ≘ T → ∀g2,Tg. ⬆*[g2] Tg ≘ T →
+ ∀f1,g1. H_at_div f2 g2 f1 g1 →
+ ∃∃T0. ⬆*[f1] T0 ≘ Tf & ⬆*[g1] T0 ≘ Tg.
+#f2 #Tf #T #H elim H -f2 -Tf -T
+[ #f2 #s #g2 #Tg #H #f1 #g1 #_
+ lapply (lifts_inv_sort2 … H) -H #H destruct
+ /2 width=3 by ex2_intro/
+| #f2 #jf #j #Hf2 #g2 #Tg #H #f1 #g1 #H0
+ elim (lifts_inv_lref2 … H) -H #jg #Hg2 #H destruct
+ elim (H0 … Hf2 Hg2) -H0 -j /3 width=3 by lifts_lref, ex2_intro/
+| #f2 #l #g2 #Tg #H #f1 #g1 #_
+ lapply (lifts_inv_gref2 … H) -H #H destruct
+ /2 width=3 by ex2_intro/
+| #f2 #p #I #Vf #V #Tf #T #_ #_ #IHV #IHT #g2 #X #H #f1 #g1 #H0
+ elim (lifts_inv_bind2 … H) -H #Vg #Tg #HVg #HTg #H destruct
+ elim (IHV … HVg … H0) -IHV -HVg
+ elim (IHT … HTg) -IHT -HTg [ |*: /2 width=8 by at_div_pp/ ]
+ /3 width=5 by lifts_bind, ex2_intro/
+| #f2 #I #Vf #V #Tf #T #_ #_ #IHV #IHT #g2 #X #H #f1 #g1 #H0
+ elim (lifts_inv_flat2 … H) -H #Vg #Tg #HVg #HTg #H destruct
+ elim (IHV … HVg … H0) -IHV -HVg
+ elim (IHT … HTg … H0) -IHT -HTg -H0
+ /3 width=5 by lifts_flat, ex2_intro/