X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpm_fpb.ma;h=66df1dcf7888b8a475bced0a921b2cd54943191b;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=0cbf9b071540f37b32e4747f873fce7843bb9cc3;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma
index 0cbf9b071..66df1dcf7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fpb.ma
@@ -22,5 +22,5 @@ include "basic_2/rt_transition/cpm_cpx.ma".
 (* Basic_2A1: includes: cpr_fpbq *)
 (* Basic_2A1: uses: cpm_fpbq *)
 lemma cpm_fwd_fpb (h) (n) (G) (L):
-      ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,n] T2 → ❪G,L,T1❫ ≽ ❪G,L,T2❫.
+      ∀T1,T2. ❨G,L❩ ⊢ T1 ➡[h,n] T2 → ❨G,L,T1❩ ≽ ❨G,L,T2❩.
 /3 width=3 by cpx_fpb, cpm_fwd_cpx/ qed-.