+lemma ldrop_fwd_rfw: ∀I,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ♯{K, V} < ♯{L, #i}.
+#I #L #K #V #i #HLK lapply (ldrop_fwd_lw … HLK) -HLK
+normalize in ⊢ (%→?%%); /2 width=1 by le_S_S/
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+fact ldrop_inv_O2_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 → e = 0 → L1 = L2.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e
+[ //
+| //
+| #I #L1 #L2 #V #e #_ #_ >commutative_plus normalize #H destruct
+| #I #L1 #L2 #V1 #V2 #d #e #_ #HV21 #IHL12 #H
+ >(IHL12 H) -L1 >(lift_inv_O2_aux … HV21 … H) -V2 -d -e //
+]
+qed-.
+
+(* Basic_1: was: drop_gen_refl *)
+lemma ldrop_inv_O2: ∀L1,L2,s,d. ⇩[s, d, 0] L1 ≡ L2 → L1 = L2.
+/2 width=5 by ldrop_inv_O2_aux/ qed-.
+
+lemma ldrop_inv_length_eq: ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ L2 → |L1| = |L2| → e = 0.
+#L1 #L2 #d #e #H #HL12 lapply (ldrop_fwd_length_minus4 … H) //
+qed-.
+
+lemma ldrop_inv_refl: ∀L,d,e. ⇩[Ⓕ, d, e] L ≡ L → e = 0.
+/2 width=5 by ldrop_inv_length_eq/ qed-.
+
+fact ldrop_inv_FT_aux: ∀L1,L2,s,d,e. ⇩[s, d, e] L1 ≡ L2 →
+ ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → d = 0 →
+ ⇩[Ⓕ, d, e] L1 ≡ K.ⓑ{I}V.
+#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e
+[ #d #e #_ #J #K #W #H destruct
+| #I #L #V #J #K #W #H destruct //
+| #I #L1 #L2 #V #e #_ #IHL12 #J #K #W #H1 #H2 destruct
+ /3 width=1 by ldrop_drop/
+| #I #L1 #L2 #V1 #V2 #d #e #_ #_ #_ #J #K #W #_ #_
+ <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma ldrop_inv_FT: ∀I,L,K,V,e. ⇩[Ⓣ, 0, e] L ≡ K.ⓑ{I}V → ⇩[e] L ≡ K.ⓑ{I}V.
+/2 width=5 by ldrop_inv_FT_aux/ qed.
+
+lemma ldrop_inv_gen: ∀I,L,K,V,s,e. ⇩[s, 0, e] L ≡ K.ⓑ{I}V → ⇩[e] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by ldrop_inv_FT/
+qed-.
+
+lemma ldrop_inv_T: ∀I,L,K,V,s,e. ⇩[Ⓣ, 0, e] L ≡ K.ⓑ{I}V → ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
+#I #L #K #V * /2 width=1 by ldrop_inv_FT/
+qed-.
+