X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbs_cpx.ma;h=caa5785b10d052ac284dd6b57fe20025d5571d01;hb=80ecd5486c6013f6c297173f41432fd1d93814ef;hp=4225caf0eaf6aba8dca86a77d0e4126cf79a8cee;hpb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
index 4225caf0e..caa5785b1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma
@@ -23,9 +23,9 @@ include "basic_2/rt_computation/fpbs_lpxs.ma".
 lemma fpbs_cpx_tneqg_trans (S):
       reflexive … S → symmetric … S → Transitive … S →
       (∀s1,s2. Decidable (S s1 s2)) →
-      ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫ →
-      ∀U2. ❪G2,L2❫ ⊢ T2 ⬈ U2 → (T2 ≛[S] U2 → ⊥) →
-      ∃∃U1. ❪G1,L1❫ ⊢ T1 ⬈ U1 & T1 ≛[S] U1 → ⊥ & ❪G1,L1,U1❫ ≥ ❪G2,L2,U2❫.
+      ∀G1,G2,L1,L2,T1,T2. ❨G1,L1,T1❩ ≥ ❨G2,L2,T2❩ →
+      ∀U2. ❨G2,L2❩ ⊢ T2 ⬈ U2 → (T2 ≛[S] U2 → ⊥) →
+      ∃∃U1. ❨G1,L1❩ ⊢ T1 ⬈ U1 & T1 ≛[S] U1 → ⊥ & ❨G1,L1,U1❩ ≥ ❨G2,L2,U2❩.
 #S #H1S #H2S #H3S #H4S #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2
 elim (fpbs_inv_star S … H) -H // #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32
 lapply (feqg_cpx_trans_cpx … H32 … HTU2) // #HTU32