-theorem drop_trans_le: ∀L1,L,s1,d1,e1. ⬇[s1, d1, e1] L1 ≡ L →
- ∀L2,s2,e2. ⬇[s2, 0, e2] L ≡ L2 → e2 ≤ d1 →
- ∃∃L0. ⬇[s2, 0, e2] L1 ≡ L0 & ⬇[s1, d1 - e2, e1] L0 ≡ L2.
-#L1 #L #s1 #d1 #e1 #H elim H -L1 -L -d1 -e1
-[ #d1 #e1 #He1 #L2 #s2 #e2 #H #_ elim (drop_inv_atom1 … H) -H
- #H #He2 destruct /4 width=3 by drop_atom, ex2_intro/
-| #I #K #V #L2 #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+theorem drop_trans_le: ∀L1,L,s1,l1,m1. ⬇[s1, l1, m1] L1 ≡ L →
+ ∀L2,s2,m2. ⬇[s2, 0, m2] L ≡ L2 → m2 ≤ l1 →
+ ∃∃L0. ⬇[s2, 0, m2] L1 ≡ L0 & ⬇[s1, l1 - m2, m1] L0 ≡ L2.
+#L1 #L #s1 #l1 #m1 #H elim H -L1 -L -l1 -m1
+[ #l1 #m1 #Hm1 #L2 #s2 #m2 #H #_ elim (drop_inv_atom1 … H) -H
+ #H #Hm2 destruct /4 width=3 by drop_atom, ex2_intro/
+| #I #K #V #L2 #s2 #m2 #HL2 #H lapply (le_n_O_to_eq … H) -H