lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩; cs] L1 ≡ L2 →
∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
/2 width=3 by drops_inv_cons_aux/ qed-.
lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, ❨l, m❩; cs] L1 ≡ L2 →
∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
/2 width=3 by drops_inv_cons_aux/ qed-.