-lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
- ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
+lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
+#L elim L -L
+[ #i #H elim (lt_zero_false … H)
+| #L #I #V #IHL #i @(nat_ind_plus … i) -i /2 width=4/ #i #_ #H
+ lapply (lt_plus_to_lt_l … H) -H #Hi
+ elim (IHL i ?) // /3 width=4/
+]
+qed.
+
+lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀K2,V,i. ⇩[0, i] L2 ≡ K2. ⓓV →