X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg_cpm.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg_cpm.ma;h=af1ef01587479de54175aea63515549c2d7b2ed5;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=82c1b2f63832583ca1031278450c0945ae078265;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma
index 82c1b2f63..af1ef0158 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_cpm.ma
@@ -21,7 +21,7 @@ include "basic_2/rt_computation/fpbg_fqup.ma".
 (* Properties with t-bound rt-transition for terms **************************)
 
 lemma cpm_tneqx_cpm_fpbg (h) (G) (L):
-      ∀n1,T1,T. ❪G,L❫ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
-      ∀n2,T2. ❪G,L❫ ⊢ T ➡[h,n2] T2 → ❪G,L,T1❫ > ❪G,L,T2❫.
+      ∀n1,T1,T. ❨G,L❩ ⊢ T1 ➡[h,n1] T → (T1 ≅ T → ⊥) →
+      ∀n2,T2. ❨G,L❩ ⊢ T ➡[h,n2] T2 → ❨G,L,T1❩ > ❨G,L,T2❩.
 /4 width=5 by fpbc_fpbs_fpbg, fpb_fpbs, cpm_fwd_fpbc, cpm_fwd_fpb/
 qed.