-lemma drops_inv_cons: â\88\80L1,L2,s,d,e,des. â\87©*[s, {d, e} @ des] L1 ≡ L2 →
- â\88\83â\88\83L. â\87©*[s, des] L1 â\89¡ L & â\87©[s, d, e] L ≡ L2.
+lemma drops_inv_cons: â\88\80L1,L2,s,d,e,des. â¬\87*[s, {d, e} @ des] L1 ≡ L2 →
+ â\88\83â\88\83L. â¬\87*[s, des] L1 â\89¡ L & â¬\87[s, d, e] L ≡ L2.