-lemma lleq_leq_repl: â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 â\86\92 â\88\80K1. K1 â\89\83[d, ∞] L1 →
- â\88\80K2. L2 â\89\83[d, ∞] K2 → K1 ≡[T, d] K2.
+lemma lleq_leq_repl: â\88\80L1,L2,T,d. L1 â\89¡[T, d] L2 â\86\92 â\88\80K1. K1 ⩬[d, ∞] L1 →
+ â\88\80K2. L2 ⩬[d, ∞] K2 → K1 ≡[T, d] K2.