- ∀b,f,I,K2,V. ⬇*[b,f] L2 ≡ K2.ⓑ{I}V → 𝐔⦃f⦄ →
- ∀f1. f ~⊚ ⫯f1 ≡ f2 →
- ∃∃K1. ⬇*[b,f] L1 ≡ K1.ⓑ{I}V & K1 ≡[f1] K2.
-#f2 #L1 #L2 #HL12 #b #f #I #K1 #V #HLK1 #Hf #f1 #Hf2
-elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -f2 -L2 -Hf
+ ∀b,f,I,K2. ⬇*[b, f] L2 ≘ K2.ⓘ{I} → 𝐔⦃f⦄ →
+ ∀f1. f ~⊚ ↑f1 ≘ f2 →
+ ∃∃K1. ⬇*[b, f] L1 ≘ K1.ⓘ{I} & K1 ≡[f1] K2.
+#f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2
+elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf
+#I1 #K1 #HLK1 #HK12 #H <(ceq_ext_inv_eq … H) -I2