X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffeqg_feqg.ma;h=1d0e4e38ff6240aacfee93fa0d18fbf64d37de34;hb=e0c91d8a4422da0b39aca790e5826dc8a617b303;hp=7a3339a88fc2fc2efcbf6c8e45c627e8f9728d2f;hpb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma
index 7a3339a88..1d0e4e38f 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/feqg_feqg.ma
@@ -28,7 +28,7 @@ qed-.
 
 lemma feqg_dec (S):
       (∀s1,s2. Decidable … (S s1 s2)) →
-      ∀G1,G2,L1,L2,T1,T2. Decidable (❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫).
+      ∀G1,G2,L1,L2,T1,T2. Decidable (❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩).
 #S #HS #G1 #G2 #L1 #L2 #T1 #T2
 elim (eq_genv_dec G1 G2) #HnG destruct
 [ elim (reqg_dec … HS L1 L2 T1) #HnL
@@ -53,20 +53,20 @@ qed-.
 
 theorem feqg_canc_sn (S):
         reflexive … S → symmetric … S → Transitive … S →
-        ∀G,G1,L,L1,T,T1. ❪G,L,T❫ ≛[S] ❪G1,L1,T1❫ →
-        ∀G2,L2,T2. ❪G,L,T❫ ≛[S] ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
+        ∀G,G1,L,L1,T,T1. ❨G,L,T❩ ≛[S] ❨G1,L1,T1❩ →
+        ∀G2,L2,T2. ❨G,L,T❩ ≛[S] ❨G2,L2,T2❩ → ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩.
 /3 width=5 by feqg_trans, feqg_sym/ qed-.
 
 theorem feqg_canc_dx (S):
         reflexive … S → symmetric … S → Transitive … S →
-        ∀G1,G,L1,L,T1,T. ❪G1,L1,T1❫ ≛[S] ❪G,L,T❫ →
-        ∀G2,L2,T2. ❪G2,L2,T2❫ ≛[S] ❪G,L,T❫ → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
+        ∀G1,G,L1,L,T1,T. ❨G1,L1,T1❩ ≛[S] ❨G,L,T❩ →
+        ∀G2,L2,T2. ❨G2,L2,T2❩ ≛[S] ❨G,L,T❩ → ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩.
 /3 width=5 by feqg_trans, feqg_sym/ qed-.
 
 lemma feqg_reqg_trans (S) (G2) (L) (T2):
       reflexive … S → symmetric … S → Transitive … S →
-      ∀G1,L1,T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L,T2❫ →
-      ∀L2. L ≛[S,T2] L2 → ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T2❫.
+      ∀G1,L1,T1. ❨G1,L1,T1❩ ≛[S] ❨G2,L,T2❩ →
+      ∀L2. L ≛[S,T2] L2 → ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T2❩.
 #S #G2 #L #T2 #H1S #H2S #H3S #G1 #L1 #T1 #H1 #L2 #HL2
 /4 width=5 by feqg_trans, feqg_intro_sn, teqg_refl/
 qed-.
@@ -76,7 +76,7 @@ qed-.
 (* Basic_2A1: uses: feqg_tneqg_repl_dx *)
 lemma feqg_tneqg_trans (S) (G1) (G2) (L1) (L2) (T):
       reflexive … S → symmetric … S → Transitive … S →
-      ∀T1. ❪G1,L1,T1❫ ≛[S] ❪G2,L2,T❫ →
+      ∀T1. ❨G1,L1,T1❩ ≛[S] ❨G2,L2,T❩ →
       ∀T2. (T ≛[S] T2 → ⊥) → (T1 ≛[S] T2 → ⊥).
 #S #G1 #G2 #L1 #L2 #T #H1S #H2S #H3S #T1 #H1 #T2 #HnT2 #HT12
 elim (feqg_inv_gen_sn … H1) -H1 #_ #_ #HnT1 -G1 -G2 -L1 -L2