X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpx_req.ma;h=5f0c34f6c84e2a8f51efe0bb22c9deb930ecea99;hp=b0d2b9922cbacc2ec13dd63e7916f95797708256;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
index b0d2b9922..5f0c34f6c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma
@@ -50,8 +50,8 @@ lemma req_cpx_trans: ∀h,G. req_transitive (cpx h G).
 qed-.
 (*
 (* 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.
+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_sn *)
@@ -59,7 +59,7 @@ lemma cpx_req_conf_sn: ∀h,G. s_r_confluent1 … (cpx h G) req.
 /2 width=5 by cpx_rex_conf/ qed-.
 (*
 (* Basic_2A1: was: cpx_lleq_conf_dx *)
-lemma cpx_req_conf_dx: ∀h,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ⬈[h] T2 →
+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-.
 *)