X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Ffpbc_lpx.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Ffpbc_lpx.ma;h=8960e8b368260b650956a2744f1ec8d6a526d966;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=5db9f7e135b12279bc5cebe5761e79c8494c3b0e;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma
index 5db9f7e13..8960e8b36 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpbc_lpx.ma
@@ -21,16 +21,16 @@ include "basic_2/rt_transition/fpbc.ma".
 
 (* Basic_2A1: uses: fpb_lpx *)
 lemma lpx_fpbc (G) (T):
-      ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → ❪G,L1,T❫ ≻ ❪G,L2,T❫.
+      ∀L1,L2. ❨G,L1❩ ⊢ ⬈ L2 → (L1 ≅[T] L2 → ⊥) → ❨G,L1,T❩ ≻ ❨G,L2,T❩.
 /3 width=1 by rpx_fpbc, lpx_rpx/ qed.
 
 (* Forward lemmas with extended rt-transition for full local envs ***********)
 
 lemma fpbc_fwd_lpx (G1) (G2) (L1) (L2) (T1) (T2):
-      ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫ →
-      ∨∨ ∃∃G,L,T. ❪G1,L1,T1❫ ⬂ ❪G,L,T❫ & ❪G,L,T❫ ≽ ❪G2,L2,T2❫
-       | ∃∃T. ❪G1,L1❫ ⊢ T1 ⬈ T & T1 ≅ T → ⊥ & ❪G1,L1,T❫ ≽ ❪G2,L2,T2❫
-       | ∃∃L. ❪G1,L1❫ ⊢ ⬈ L & (L1 ≅[T1] L → ⊥) & ❪G1,L,T1❫ ≽ ❪G2,L2,T2❫.
+      ❨G1,L1,T1❩ ≻ ❨G2,L2,T2❩ →
+      ∨∨ ∃∃G,L,T. ❨G1,L1,T1❩ ⬂ ❨G,L,T❩ & ❨G,L,T❩ ≽ ❨G2,L2,T2❩
+       | ∃∃T. ❨G1,L1❩ ⊢ T1 ⬈ T & T1 ≅ T → ⊥ & ❨G1,L1,T❩ ≽ ❨G2,L2,T2❩
+       | ∃∃L. ❨G1,L1❩ ⊢ ⬈ L & (L1 ≅[T1] L → ⊥) & ❨G1,L,T1❩ ≽ ❨G2,L2,T2❩.
 #G1 #G2 #L1 #L2 #T1 #T2 #H
 elim (fpbc_inv_gen sfull … H) -H #H12 #Hn12
 elim (fpb_inv_gen … H12) -H12 #L #T #H1 #HT2 #HL2