-lemma lsreds_inv_pos: â\88\80s,M1,M2. M1 â\87\80*[s] M2 → 0 < |s| →
- â\88\83â\88\83p,r,M. p::r = s & M1 â\87\80[p] M & M â\87\80*[r] M2.
+lemma lsreds_inv_pos: â\88\80s,M1,M2. M1 â\86¦*[s] M2 → 0 < |s| →
+ â\88\83â\88\83p,r,M. p::r = s & M1 â\86¦[p] M & M â\86¦*[r] M2.