lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
|L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
#K #L1 #L2 elim L2 -L2 normalize //
lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
|L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
#K #L1 #L2 elim L2 -L2 normalize //