-lemma ldrop_append_O1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
- |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
+fact ldrop_O1_append_sn_le_aux: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+ d = 0 → e ≤ |L1| →
+ ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // /4 width=1/
+#d #e #_ #H #L -d
+lapply (le_n_O_to_eq … H) -H //
+qed-.
+
+lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
+ ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
+/2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
+
+(* Inversion lemmas on append for local environments ************************)
+
+lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
+ |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.