X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_fpb.ma;h=c2ab3ea6aa37ac63b11a70d3d859ef761336b30c;hb=e0c91d8a4422da0b39aca790e5826dc8a617b303;hp=5c69219b20ae386f9e3cc3e496950b8328def46f;hpb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma
index 5c69219b2..c2ab3ea6a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpb.ma
@@ -23,8 +23,8 @@ include "basic_2/rt_computation/csx_lpx.ma".
 
 (* Basic_2A1: was: csx_fpb_conf *)
 lemma csx_fpb_conf:
-      ∀G1,L1,T1. ❪G1,L1❫ ⊢ ⬈*𝐒 T1 →
-      ∀G2,L2,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ → ❪G2,L2❫ ⊢ ⬈*𝐒 T2.
+      ∀G1,L1,T1. ❨G1,L1❩ ⊢ ⬈*𝐒 T1 →
+      ∀G2,L2,T2. ❨G1,L1,T1❩ ≽ ❨G2,L2,T2❩ → ❨G2,L2❩ ⊢ ⬈*𝐒 T2.
 #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H
 elim (fpb_inv_req … H) -H #L0 #L #T #H1 #HT2 #HL0 #HL02
 lapply (cpx_reqg_conf … HL0 … HT2) -HT2 // #HT2