-theorem ldrop_trans_le: ∀d1,e1,L1,L. ⇩[d1, e1] L1 ≡ L →
- ∀e2,L2. ⇩[0, e2] L ≡ L2 → e2 ≤ d1 →
- ∃∃L0. ⇩[0, e2] L1 ≡ L0 & ⇩[d1 - e2, e1] L0 ≡ L2.
-#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
-[ #d #e2 #L2 #H
- elim (ldrop_inv_atom1 … H) -H /2 width=3 by ldrop_atom, ex2_intro/
-| #K #I #V #e2 #L2 #HL2 #H
- lapply (le_n_O_to_eq … H) -H #H destruct /2 width=3 by ldrop_pair, ex2_intro/
-| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
- lapply (le_n_O_to_eq … H) -H #H destruct
- elim (IHL12 … HL2) -IHL12 -HL2 // #L0 #H #HL0
- lapply (ldrop_inv_O2 … H) -H #H destruct /3 width=5 by ldrop_pair, ldrop_ldrop, ex2_intro/
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
+theorem ldrop_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 (ldrop_inv_atom1 … H) -H
+ #H #He2 destruct /4 width=3 by ldrop_atom, ex2_intro/
+| #I #K #V #L2 #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+ #H destruct /2 width=3 by ldrop_pair, ex2_intro/
+| #I #L1 #L2 #V #e #_ #IHL12 #L #s2 #e2 #HL2 #H lapply (le_n_O_to_eq … H) -H
+ #H destruct elim (IHL12 … HL2) -IHL12 -HL2 //
+ #L0 #H #HL0 lapply (ldrop_inv_O2 … H) -H #H destruct
+ /3 width=5 by ldrop_pair, ldrop_drop, ex2_intro/
+| #I #L1 #L2 #V1 #V2 #d #e #HL12 #HV12 #IHL12 #L #s2 #e2 #H #He2d