| drops_nil : ∀L. drops s (◊) L L
| drops_cons: ∀L1,L,L2,cs,l,m.
drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2
| drops_nil : ∀L. drops s (◊) L L
| drops_cons: ∀L1,L,L2,cs,l,m.
drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2