+ #e #_ normalize #H elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
+]
+qed-.
+
+lemma ldrop_O1_pair: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → e ≤ |L| → ∀I,V.
+ ∃∃J,W. ⇩[s, 0, e] L.ⓑ{I}V ≡ K.ⓑ{J}W.
+#L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize #He #I #V
+[ elim (ldrop_inv_atom1 … H) -H #H <(le_n_O_to_eq … He) -e
+ #Hs destruct /2 width=3 by ex1_2_intro/
+| elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK destruct /2 width=3 by ex1_2_intro/
+ elim (IHL … HLK … Z X) -IHL -HLK
+ /3 width=3 by ldrop_drop_lt, le_plus_to_minus, ex1_2_intro/
+]
+qed-.
+
+lemma ldrop_O1_ge: ∀L,e. |L| ≤ e → ⇩[Ⓣ, 0, e] L ≡ ⋆.
+#L elim L -L [ #e #_ @ldrop_atom #H destruct ]
+#L #I #V #IHL #e @(nat_ind_plus … e) -e [ #H elim (le_plus_xSy_O_false … H) ]
+normalize /4 width=1 by ldrop_drop, monotonic_pred/
+qed.
+
+lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 →
+ ∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2.
+#L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2
+[ #d #e2 #Hs #e1 #He12 @(ex2_intro … (⋆))
+ @ldrop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
+| #I #L1 #V #e1 #He1 lapply (le_n_O_to_eq … He1) -He1
+ #H destruct /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #e2 #HL12 #IHL12 #e1 @(nat_ind_plus … e1) -e1
+ [ /3 width=3 by ldrop_drop, ex2_intro/
+ | -HL12 #e1 #_ #He12 lapply (le_plus_to_le_r … He12) -He12
+ #He12 elim (IHL12 … He12) -IHL12 >minus_plus_plus_l
+ #L #HL1 #HL2 elim (lt_or_ge (|L1|) (e2-e1)) #H0
+ [ elim (ldrop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
+ elim (ldrop_inv_atom1 … HL2) -HL2 #H #_ destruct
+ @(ex2_intro … (⋆)) [ @ldrop_O1_ge normalize // ]
+ @ldrop_atom #H destruct
+ | elim (ldrop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by ldrop_drop, ex2_intro/
+ ]
+ ]
+| #I #L1 #L2 #V1 #V2 #d #e2 #_ #HV21 #IHL12 #e1 #He12 elim (IHL12 … He12) -IHL12
+ #L #HL1 #HL2 elim (lift_split … HV21 d e1) -HV21 /3 width=5 by ldrop_skip, ex2_intro/