/3 width=6 by cpx_rex_conf/ qed-.
(* Basic_2A1: was just: cpx_lleq_conf_dx *)
-lemma cpx_reqx_conf_dx: â\88\80h,G,L2,T1,T2. â¦\83G,L2â¦\84 ⊢ T1 ⬈[h] T2 →
+lemma cpx_reqx_conf_dx: â\88\80h,G,L2,T1,T2. â\9dªG,L2â\9d« ⊢ T1 ⬈[h] T2 →
∀L1. L1 ≛[T1] L2 → L1 ≛[T2] L2.
/4 width=5 by cpx_reqx_conf_sn, reqx_sym/ qed-.