-fact drop_O1_append_sn_le_aux: ∀L1,L2,s,d,e. ⬇[s, d, e] L1 ≡ L2 →
- d = 0 → e ≤ |L1| →
- ∀L. ⬇[s, 0, e] L @@ L1 ≡ L @@ L2.
-#L1 #L2 #s #d #e #H elim H -L1 -L2 -d -e normalize
+fact drop_O1_append_sn_le_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 →
+ l = 0 → m ≤ |L1| →
+ ∀L. ⬇[s, 0, m] L @@ L1 ≡ L @@ L2.
+#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m normalize