--- /dev/null
+(* 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-.