-lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 →
- ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2.
-/2 width=3/ qed-.
+lemma ldrops_inv_cons: ∀L1,L2,s,d,e,des. ⇩*[s, {d, e} @ des] L1 ≡ L2 →
+ ∃∃L. ⇩*[s, des] L1 ≡ L & ⇩[s, d, e] L ≡ L2.
+/2 width=3 by ldrops_inv_cons_aux/ qed-.