X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_fqup.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Ffrees_fqup.ma;h=2534a671c5cfce4fd1f575c572079036fd26d1b2;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=6868962e64f6782e5a0dacd64b41f796a7408610;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
index 6868962e6..2534a671c 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
@@ -20,7 +20,7 @@ include "static_2/static/lsubf_lsubr.ma".
 (* Advanced properties ******************************************************)
 
 (* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+❪T❫ ≘ f.
+lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+❨T❩ ≘ f.
 #L #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L T) -L -T
 #G0 #L0 #T0 #IH #G #L * *
 [ /3 width=2 by frees_sort, ex_intro/
@@ -52,8 +52,8 @@ qed-.
 (* Advanced main properties *************************************************)
 
 theorem frees_bind_void:
-        ∀f1,L,V. L ⊢ 𝐅+❪V❫ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 →
-        ∀f. f1 ⋓ ⫰f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
+        ∀f1,L,V. L ⊢ 𝐅+❨V❩ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❨T❩ ≘ f2 →
+        ∀f. f1 ⋓ ⫰f2 ≘ f → ∀p,I. L ⊢ 𝐅+❨ⓑ[p,I]V.T❩ ≘ f.
 #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
 elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
@@ -80,8 +80,8 @@ qed-.
 (* Advanced inversion lemmas ************************************************)
 
 lemma frees_inv_bind_void:
-      ∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
-      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
+      ∀f,p,I,L,V,T. L ⊢ 𝐅+❨ⓑ[p,I]V.T❩ ≘ f →
+      ∃∃f1,f2. L ⊢ 𝐅+❨V❩ ≘ f1 & L.ⓧ ⊢ 𝐅+❨T❩ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
 #f #p #I #L #V #T #H
 elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
 elim (frees_total (L.ⓧ) T) #f0 #Hf0
@@ -104,29 +104,29 @@ qed-.
 
 lemma frees_ind_void (Q:relation3 …):
       (
-        ∀f,L,s. 𝐈❪f❫ →  Q L (⋆s) f
+        ∀f,L,s. 𝐈❨f❩ →  Q L (⋆s) f
       ) → (
-        ∀f,i. 𝐈❪f❫ →  Q (⋆) (#i) (⫯*[i]↑f)
+        ∀f,i. 𝐈❨f❩ →  Q (⋆) (#i) (⫯*[i]↑f)
       ) → (
         ∀f,I,L,V.
-        L ⊢ 𝐅+❪V❫ ≘ f →  Q L V f→ Q (L.ⓑ[I]V) (#O) (↑f)
+        L ⊢ 𝐅+❨V❩ ≘ f →  Q L V f→ Q (L.ⓑ[I]V) (#O) (↑f)
       ) → (
-        ∀f,I,L. 𝐈❪f❫ →  Q (L.ⓤ[I]) (#O) (↑f)
+        ∀f,I,L. 𝐈❨f❩ →  Q (L.ⓤ[I]) (#O) (↑f)
       ) → (
         ∀f,I,L,i.
-        L ⊢ 𝐅+❪#i❫ ≘ f →  Q L (#i) f → Q (L.ⓘ[I]) (#(↑i)) (⫯f)
+        L ⊢ 𝐅+❨#i❩ ≘ f →  Q L (#i) f → Q (L.ⓘ[I]) (#(↑i)) (⫯f)
       ) → (
-        ∀f,L,l. 𝐈❪f❫ →  Q L (§l) f
+        ∀f,L,l. 𝐈❨f❩ →  Q L (§l) f
       ) → (
         ∀f1,f2,f,p,I,L,V,T.
-        L ⊢ 𝐅+❪V❫ ≘ f1 → L.ⓧ ⊢𝐅+❪T❫≘ f2 → f1 ⋓ ⫰f2 ≘ f →
+        L ⊢ 𝐅+❨V❩ ≘ f1 → L.ⓧ ⊢𝐅+❨T❩≘ f2 → f1 ⋓ ⫰f2 ≘ f →
         Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f
       ) → (
         ∀f1,f2,f,I,L,V,T.
-        L ⊢ 𝐅+❪V❫ ≘ f1 → L ⊢𝐅+❪T❫ ≘ f2 → f1 ⋓ f2 ≘ f →
+        L ⊢ 𝐅+❨V❩ ≘ f1 → L ⊢𝐅+❨T❩ ≘ f2 → f1 ⋓ f2 ≘ f →
         Q L V f1 → Q L T f2 → Q L (ⓕ[I]V.T) f
       ) →
-      ∀L,T,f. L ⊢ 𝐅+❪T❫ ≘ f →  Q L T f.
+      ∀L,T,f. L ⊢ 𝐅+❨T❩ ≘ f →  Q L T f.
 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #L #T
 @(fqup_wf_ind_eq (Ⓕ) … (⋆) L T) -L -T #G0 #L0 #T0 #IH #G #L * *
 [ #s #HG #HL #HT #f #H destruct -IH