+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/
+]
+qed-.
+
+lemma lifts_div4_one: ∀f,Tf,T. ⬆*[⫯f] Tf ≘ T →
+ ∀T1. ⬆*[1] T1 ≘ T →
+ ∃∃T0. ⬆*[1] T0 ≘ Tf & ⬆*[f] T0 ≘ T1.
+/4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-.
+
+theorem lifts_div3: ∀f2,T,T2. ⬆*[f2] T2 ≘ T → ∀f,T1. ⬆*[f] T1 ≘ T →
+ ∀f1. f2 ⊚ f1 ≘ f → ⬆*[f1] T1 ≘ T2.