update in basic_2 and ground_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / frees_fqup.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
index e7fcf4eb854d1485e2bf903445e675d7127743e7..8946c6e4a2f59636a34f1c9f2aa9068cb706af1c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -20,7 +20,7 @@ include "basic_2/static/lsubf_lsubr.ma".
 (* Advanced properties ******************************************************)
 
 (* Note: this replaces lemma 1400 concluding the "big tree" theorem *)
-lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f.
+lemma frees_total: â\88\80L,T. â\88\83f. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 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/
@@ -51,8 +51,8 @@ qed-.
 
 (* Advanced main properties *************************************************)
 
-theorem frees_bind_void: â\88\80f1,L,V. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 →
-                         â\88\80f. f1 â\8b\93 ⫱f2 â\89¡ f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89¡ f.
+theorem frees_bind_void: â\88\80f1,L,V. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 â\86\92 â\88\80f2,T. L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 →
+                         â\88\80f. f1 â\8b\93 ⫱f2 â\89\98 f â\86\92 â\88\80p,I. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89\98 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
@@ -78,8 +78,8 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma frees_inv_bind_void: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89¡ f →
-                           â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+lemma frees_inv_bind_void: â\88\80f,p,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\91{p,I}V.Tâ¦\84 â\89\98 f →
+                           â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L.â\93§ â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 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
@@ -107,24 +107,24 @@ lemma frees_ind_void: ∀R:relation3 ….
                          ∀f,i. 𝐈⦃f⦄ → R (⋆) (#i) (↑*[i]⫯f)
                       ) → (
                          ∀f,I,L,V.
-                         L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f → R L V f→ R (L.ⓑ{I}V) (#O) (⫯f) 
+                         L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f → R L V f→ R (L.ⓑ{I}V) (#O) (⫯f) 
                       ) → (
                          ∀f,I,L. 𝐈⦃f⦄ → R (L.ⓤ{I}) (#O) (⫯f)
                       ) → (
                          ∀f,I,L,i.
-                         L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ f → R L (#i) f → R (L.ⓘ{I}) (#(⫯i)) (↑f)
+                         L â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f → R L (#i) f → R (L.ⓘ{I}) (#(⫯i)) (↑f)
                       ) → (
                          ∀f,L,l. 𝐈⦃f⦄ → R L (§l) f
                       ) → (
                          ∀f1,f2,f,p,I,L,V,T.
-                         L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85*â¦\83Tâ¦\84â\89¡ f2 â\86\92 f1 â\8b\93 ⫱f2 â\89¡ f →
+                         L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 â\86\92 L.â\93§ â\8a¢ð\9d\90\85*â¦\83Tâ¦\84â\89\98 f2 â\86\92 f1 â\8b\93 ⫱f2 â\89\98 f →
                          R L V f1 →R (L.ⓧ) T f2 → R L (ⓑ{p,I}V.T) f
                       ) → (
                          ∀f1,f2,f,I,L,V,T.
-                         L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 â\86\92 L â\8a¢ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 â\86\92 f1 â\8b\93 f2 â\89¡ f →
+                         L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 â\86\92 L â\8a¢ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 â\86\92 f1 â\8b\93 f2 â\89\98 f →
                          R L V f1 → R L T f2 → R L (ⓕ{I}V.T) f
                       ) →
-                      â\88\80L,T,f. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f → R L T f.
+                      â\88\80L,T,f. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f → R L T f.
 #R #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