matita/matita/contribs/lambdadelta/basic_2/etc/cpx_req.etc

   1 (* req_req is missing, with req_sym *)
   2
   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-.
   8
   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-.