X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Ffpbc_fpb.ma;h=0c31ace7ae89630197cace00b75b6323cd588cd4;hb=829e3a8af3229c4e625245f7265dd67939da98c4;hp=35654e6da9aef042e83ae6d47959dc676cbb26d9;hpb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma
index 35654e6da..0c31ace7a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_fpb.ma
@@ -21,9 +21,9 @@ include "basic_2/rt_transition/fpbc.ma".
 
 (* Basic_2A1: uses: fpbq_ind_alt *)
 lemma fpb_inv_fpbc:
-      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
-      ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
-       | ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
+      ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≽ ❨G2,L2,T2❩ →
+      ∨∨ ❨G1,L1,T1❩ ≅ ❨G2,L2,T2❩
+       | ❨G1,L1,T1❩ ≻ ❨G2,L2,T2❩.
 #G1 #G2 #L1 #L2 #T1 #T2 #H 
 elim (feqx_dec G1 G2 L1 L2 T1 T2)
 /4 width=1 by fpbc_intro, or_intror, or_introl/