(* req_req is missing, with req_sym *)

(* Basic_2A1: was: cpx_lleq_conf *)
lemma cpx_req_conf (h) (G):
      ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
      ∀L1. L2 ≡[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
/3 width=3 by req_cpx_trans, req_sym/ qed-.

(* Basic_2A1: was: cpx_lleq_conf_dx *)
lemma cpx_req_conf_dx (h) (G):
      ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
      ∀L1. L1 ≡[T1] L2 → L1 ≡[T2] L2.
/4 width=6 by cpx_req_conf_sn, req_sym/ qed-.