X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Freqg.ma;h=f014125017f35ed59b49deb1ff1cf8963762df8a;hb=11093619476326238c2ef9d2dfe9150b8c9bc920;hp=1c5d5ed9074426338777e671831f42b7d0ed6f8f;hpb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma
index 1c5d5ed90..f01412501 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqg.ma
@@ -32,8 +32,8 @@ interpretation
 (* Basic properties ***********************************************************)
 
 lemma frees_teqg_conf_seqg (S):
-      ∀f,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f → ∀T2. T1 ≛[S] T2 →
-      ∀L2. L1 ≛[S,f] L2 → L2 ⊢ 𝐅+❪T2❫ ≘ f.
+      ∀f,L1,T1. L1 ⊢ 𝐅+❨T1❩ ≘ f → ∀T2. T1 ≛[S] T2 →
+      ∀L2. L1 ≛[S,f] L2 → L2 ⊢ 𝐅+❨T2❩ ≘ f.
 #S #f #L1 #T1 #H elim H -f -L1 -T1
 [ #f #L1 #s1 #Hf #X #H1 #L2 #_
   elim (teqg_inv_sort1 … H1) -H1 #s2 #_ #H destruct
@@ -59,23 +59,23 @@ lemma frees_teqg_conf_seqg (S):
   >(teqg_inv_gref1 … H1) -X /2 width=1 by frees_gref/
 | #f1V #f1T #f1 #p #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
   elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
-  /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+  /6 width=5 by frees_bind, sex_inv_tl, ext2_pair, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/
 | #f1V #f1T #f1 #I #L1 #V1 #T1 #_ #_ #Hf1 #IHV #IHT #X #H1
   elim (teqg_inv_pair1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H1 #L2 #HL12 destruct
-  /5 width=5 by frees_flat, sle_sex_trans, sor_inv_sle_dx, sor_inv_sle_sn/
+  /5 width=5 by frees_flat, sle_sex_trans, pr_sor_inv_sle_dx, pr_sor_inv_sle_sn/
 ]
 qed-.
 
 lemma frees_teqg_conf (S):
       reflexive … S →
-      ∀f,L,T1. L ⊢ 𝐅+❪T1❫ ≘ f →
-      ∀T2. T1 ≛[S] T2 → L ⊢ 𝐅+❪T2❫ ≘ f.
+      ∀f,L,T1. L ⊢ 𝐅+❨T1❩ ≘ f →
+      ∀T2. T1 ≛[S] T2 → L ⊢ 𝐅+❨T2❩ ≘ f.
 /5 width=6 by frees_teqg_conf_seqg, sex_refl, teqg_refl, ext2_refl/ qed-.
 
 lemma frees_seqg_conf (S):
       reflexive … S →
-      ∀f,L1,T. L1 ⊢ 𝐅+❪T❫ ≘ f →
-      ∀L2. L1 ≛[S,f] L2 → L2 ⊢ 𝐅+❪T❫ ≘ f.
+      ∀f,L1,T. L1 ⊢ 𝐅+❨T❩ ≘ f →
+      ∀L2. L1 ≛[S,f] L2 → L2 ⊢ 𝐅+❨T❩ ≘ f.
 /3 width=6 by frees_teqg_conf_seqg, teqg_refl/ qed-.
 
 lemma teqg_rex_conf_sn (S) (R):
@@ -117,7 +117,7 @@ lemma reqg_pair (S):
 /2 width=1 by rex_pair/ qed.
 
 lemma reqg_unit (S):
-      ∀f,I,L1,L2. 𝐈❪f❫ → L1 ≛[S,f] L2 →
+      ∀f,I,L1,L2. 𝐈❨f❩ → L1 ≛[S,f] L2 →
       L1.ⓤ[I] ≛[S,#0] L2.ⓤ[I].
 /2 width=3 by rex_unit/ qed.
 
@@ -155,7 +155,7 @@ lemma reqg_inv_zero (S):
       ∀Y1,Y2. Y1 ≛[S,#0] Y2 →
       ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆
        | ∃∃I,L1,L2,V1,V2. L1 ≛[S,V1] L2 & V1 ≛[S] V2 & Y1 = L1.ⓑ[I]V1 & Y2 = L2.ⓑ[I]V2
-       | ∃∃f,I,L1,L2. 𝐈❪f❫ & L1 ≛[S,f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
+       | ∃∃f,I,L1,L2. 𝐈❨f❩ & L1 ≛[S,f] L2 & Y1 = L1.ⓤ[I] & Y2 = L2.ⓤ[I].
 #S #Y1 #Y2 #H elim (rex_inv_zero … H) -H *
 /3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_4_intro, conj/
 qed-.