1 (* req_req is missing, with req_sym *)
3 (* Basic_2A1: was: cpx_lleq_conf *)
4 lemma cpx_req_conf (h) (G):
5 ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
6 ∀L1. L2 ≡[T1] L1 → ⦃G,L1⦄ ⊢ T1 ⬈[h] T2.
7 /3 width=3 by req_cpx_trans, req_sym/ qed-.
9 (* Basic_2A1: was: cpx_lleq_conf_dx *)
10 lemma cpx_req_conf_dx (h) (G):
11 ∀L2,T1,T2. ⦃G,L2⦄ ⊢ T1 ⬈[h] T2 →
12 ∀L1. L1 ≡[T1] L2 → L1 ≡[T2] L2.
13 /4 width=6 by cpx_req_conf_sn, req_sym/ qed-.