-lemma drops_lreq_trans_next: ∀K1,K2,f1. K1 ≡[f1] K2 →
- ∀I,L1,V,c,f. ⬇*[c,f] L1.ⓑ{I}V ≡ K1 →
- ∀f2. f ⊚ f1 ≡ ⫯f2 →
- ∃∃L2. ⬇*[c,f] L2.ⓑ{I}V ≡ K2 & L1 ≡[f2] L2 & L1.ⓑ{I}V≡[f]L2.ⓑ{I}V.
-#K1 #K2 #f1 #HK12 #I #L1 #V #c #f #HLK1 #f2 #Hf2
-elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -K1 -f1
-/2 width=6 by cfull_lift, ceq_lift, cfull_refl, ceq_refl, ex3_intro/
+lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 →
+ ∀b,f,I,L1. ⬇*[b, f] L1.ⓘ{I} ≘ K1 →
+ ∀f2. f ~⊚ f1 ≘ ↑f2 →
+ ∃∃L2. ⬇*[b, f] L2.ⓘ{I} ≘ K2 & L1 ≡[f2] L2 & L1.ⓘ{I} ≡[f] L2.ⓘ{I}.
+#f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2
+elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1
+/2 width=6 by cfull_lift_sn, ceq_lift_sn/
+#I2 #L2 #HLK2 #HL12 #H >(ceq_ext_inv_eq … H) -I1
+/2 width=4 by ex3_intro/