+lemma ldrop_inv_O1_pair2: ∀I,K,V,e,L1. ⇩[0, e] L1 ≡ K. ⓑ{I} V →
+ (e = 0 ∧ L1 = K. ⓑ{I} V) ∨
+ ∃∃I1,K1,V1. ⇩[0, e - 1] K1 ≡ K. ⓑ{I} V & L1 = K1.ⓑ{I1}V1 & 0 < e.
+#I #K #V #e *
+[ #H lapply (ldrop_inv_atom1 … H) -H #H destruct
+| #L1 #I1 #V1 #H
+ elim (ldrop_inv_O1 … H) -H *
+ [ #H1 #H2 destruct /3 width=1/
+ | /3 width=5/
+ ]
+]
+qed-.
+