/3 width=3 by lfdeq_cpxs_trans, lfdeq_sym/ qed-.
(* Basic_2A1: was just: cpxs_lleq_conf_dx *)
lemma cpxs_lfdeq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈*[h] T2 →
/3 width=3 by lfdeq_cpxs_trans, lfdeq_sym/ qed-.
(* Basic_2A1: was just: cpxs_lleq_conf_dx *)
lemma cpxs_lfdeq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈*[h] T2 →