-lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
- â\88\80L1. L1 â\8b\95[T1, 0] L2 â\86\92 L1 â\8b\95[T2, 0] L2.
-/4 width=6 by lleq_cpx_conf_sn, lleq_sym/ qed-.
+lemma cpx_lleq_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
+ â\88\80L1. L1 â\89¡[T1, 0] L2 â\86\92 L1 â\89¡[T2, 0] L2.
+/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-.