+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-.
+