X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Ffpb_aaa.ma;h=898ffd3f0f1be8436a1752bb79696b9badd5dcb6;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=533718941cc73546588c0b6493b4489c0b075baa;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.ma
index 533718941..898ffd3f0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_aaa.ma
@@ -23,8 +23,8 @@ include "basic_2/rt_transition/fpb_lpx.ma".
 
 (* Basic_2A1: uses: fpbq_aaa_conf *)
 lemma fpb_aaa_conf:
-      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
-      ∀A1. ❪G1,L1❫ ⊢ T1 ⁝ A1 → ∃A2. ❪G2,L2❫ ⊢ T2 ⁝ A2.
+      ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≽ ❨G2,L2,T2❩ →
+      ∀A1. ❨G1,L1❩ ⊢ T1 ⁝ A1 → ∃A2. ❨G2,L2❩ ⊢ T2 ⁝ A2.
 #G1 #G2 #L1 #L2 #T1 #T2 #H #A1 #HA1
 elim (fpb_inv_req … H) -H #L0 #L #T #H1 #HT2 #HL0 #HL02
 elim (aaa_fquq_conf … H1 … HA1) -G1 -L1 -T1 -A1 #A2 #HA2