renaming in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
index 206ec63e4b8a99a4c9d27e9417b680003970730c..b35ea99b828235e63e509e378d657cf5802ce5ed 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
@@ -20,17 +20,17 @@ include "basic_2/syntax/lenv.ma".
 
 inductive frees: relation3 lenv term rtmap ≝
 | frees_sort: ∀f,L,s. 𝐈⦃f⦄ → frees L (⋆s) f
-| frees_atom: â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 â\86\92 frees (â\8b\86) (#i) (â\86\91*[i]⫯f)
+| frees_atom: â\88\80f,i. ð\9d\90\88â¦\83fâ¦\84 â\86\92 frees (â\8b\86) (#i) (⫯*[i]â\86\91f)
 | frees_pair: ∀f,I,L,V. frees L V f →
-              frees (L.â\93\91{I}V) (#0) (⫯f)
-| frees_unit: â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92 frees (L.â\93¤{I}) (#0) (⫯f)
+              frees (L.â\93\91{I}V) (#0) (â\86\91f)
+| frees_unit: â\88\80f,I,L. ð\9d\90\88â¦\83fâ¦\84 â\86\92 frees (L.â\93¤{I}) (#0) (â\86\91f)
 | frees_lref: ∀f,I,L,i. frees L (#i) f →
-              frees (L.â\93\98{I}) (#⫯i) (â\86\91f)
+              frees (L.â\93\98{I}) (#â\86\91i) (⫯f)
 | frees_gref: ∀f,L,l. 𝐈⦃f⦄ → frees L (§l) f
 | frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ{I}V) T f2 →
-              f1 â\8b\93 ⫱f2 â\89¡ f → frees L (ⓑ{p,I}V.T) f
+              f1 â\8b\93 ⫱f2 â\89\98 f → frees L (ⓑ{p,I}V.T) f
 | frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
-              f1 â\8b\93 f2 â\89¡ f → frees L (ⓕ{I}V.T) f
+              f1 â\8b\93 f2 â\89\98 f → frees L (ⓕ{I}V.T) f
 .
 
 interpretation
@@ -39,7 +39,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact frees_inv_sort_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀x. X = ⋆x → 𝐈⦃f⦄.
+fact frees_inv_sort_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀x. X = ⋆x → 𝐈⦃f⦄.
 #L #X #f #H elim H -f -L -X //
 [ #f #i #_ #x #H destruct
 | #f #_ #L #V #_ #_ #x #H destruct
@@ -50,11 +50,11 @@ fact frees_inv_sort_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = ⋆x 
 ]
 qed-.
 
-lemma frees_inv_sort: â\88\80f,L,s. L â\8a¢ ð\9d\90\85*â¦\83â\8b\86sâ¦\84 â\89¡ f → 𝐈⦃f⦄.
+lemma frees_inv_sort: â\88\80f,L,s. L â\8a¢ ð\9d\90\85*â¦\83â\8b\86sâ¦\84 â\89\98 f → 𝐈⦃f⦄.
 /2 width=5 by frees_inv_sort_aux/ qed-.
 
-fact frees_inv_atom_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀i. L = ⋆ → X = #i →
-                         â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i]⫯g.
+fact frees_inv_atom_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀i. L = ⋆ → X = #i →
+                         â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i]â\86\91g.
 #f #L #X #H elim H -f -L -X
 [ #f #L #s #_ #j #_ #H destruct
 | #f #i #Hf #j #_ #H destruct /2 width=3 by ex2_intro/
@@ -67,11 +67,11 @@ fact frees_inv_atom_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀i. L = ⋆ 
 ]
 qed-.
 
-lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91*[i]⫯g.
+lemma frees_inv_atom: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯*[i]â\86\91g.
 /2 width=5 by frees_inv_atom_aux/ qed-.
 
-fact frees_inv_pair_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀I,K,V. L = K.ⓑ{I}V → X = #0 →
-                         â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & f = ⫯g.
+fact frees_inv_pair_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀I,K,V. L = K.ⓑ{I}V → X = #0 →
+                         â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & f = â\86\91g.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #Z #Y #X #_ #H destruct
 | #f #i #_ #Z #Y #X #H destruct
@@ -84,11 +84,11 @@ fact frees_inv_pair_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,V. L = K.
 ]
 qed-.
 
-lemma frees_inv_pair: â\88\80f,I,K,V. K.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89¡ f â\86\92 â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ g & f = ⫯g.
+lemma frees_inv_pair: â\88\80f,I,K,V. K.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 g & f = â\86\91g.
 /2 width=6 by frees_inv_pair_aux/ qed-.
 
-fact frees_inv_unit_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀I,K. L = K.ⓤ{I} → X = #0 →
-                         â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯g.
+fact frees_inv_unit_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀I,K. L = K.ⓤ{I} → X = #0 →
+                         â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91g.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #Z #Y #_ #H destruct
 | #f #i #_ #Z #Y #H destruct
@@ -101,11 +101,11 @@ fact frees_inv_unit_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K. L = K.
 ]
 qed-.
 
-lemma frees_inv_unit: â\88\80f,I,K. K.â\93¤{I} â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89¡ f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = ⫯g.
+lemma frees_inv_unit: â\88\80f,I,K. K.â\93¤{I} â\8a¢ ð\9d\90\85*â¦\83#0â¦\84 â\89\98 f â\86\92 â\88\83â\88\83g. ð\9d\90\88â¦\83gâ¦\84 & f = â\86\91g.
 /2 width=7 by frees_inv_unit_aux/ qed-.
 
-fact frees_inv_lref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f â\86\92 â\88\80I,K,j. L = K.â\93\98{I} â\86\92 X = #(⫯j) →
-                         â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#jâ¦\84 â\89¡ g & f = â\86\91g.
+fact frees_inv_lref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f â\86\92 â\88\80I,K,j. L = K.â\93\98{I} â\86\92 X = #(â\86\91j) →
+                         â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#jâ¦\84 â\89\98 g & f = ⫯g.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #Z #Y #j #_ #H destruct
 | #f #i #_ #Z #Y #j #H destruct
@@ -118,11 +118,11 @@ fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,K,j. L = K.
 ]
 qed-.
 
-lemma frees_inv_lref: â\88\80f,I,K,i. K.â\93\98{I} â\8a¢ ð\9d\90\85*â¦\83#(⫯i)â¦\84 â\89¡ f →
-                      â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ g & f = â\86\91g.
+lemma frees_inv_lref: â\88\80f,I,K,i. K.â\93\98{I} â\8a¢ ð\9d\90\85*â¦\83#(â\86\91i)â¦\84 â\89\98 f →
+                      â\88\83â\88\83g. K â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 g & f = ⫯g.
 /2 width=6 by frees_inv_lref_aux/ qed-.
 
-fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀x. X = §x → 𝐈⦃f⦄.
+fact frees_inv_gref_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀x. X = §x → 𝐈⦃f⦄.
 #f #L #X #H elim H -f -L -X //
 [ #f #i #_ #x #H destruct
 | #f #_ #L #V #_ #_ #x #H destruct
@@ -133,11 +133,11 @@ fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀x. X = §x 
 ]
 qed-.
 
-lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85*â¦\83§lâ¦\84 â\89¡ f → 𝐈⦃f⦄.
+lemma frees_inv_gref: â\88\80f,L,l. L â\8a¢ ð\9d\90\85*â¦\83§lâ¦\84 â\89\98 f → 𝐈⦃f⦄.
 /2 width=5 by frees_inv_gref_aux/ qed-.
 
-fact frees_inv_bind_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
-                         â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+fact frees_inv_bind_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀p,I,V,T. X = ⓑ{p,I}V.T →
+                         â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L.â\93\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 f.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #q #J #W #U #H destruct
 | #f #i #_ #q #J #W #U #H destruct
@@ -150,12 +150,12 @@ fact frees_inv_bind_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀p,I,V,T. X =
 ]
 qed-.
 
-lemma frees_inv_bind: â\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\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 ⫱f2 â\89¡ f.
+lemma frees_inv_bind: â\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\91{I}V â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 ⫱f2 â\89\98 f.
 /2 width=4 by frees_inv_bind_aux/ qed-.
 
-fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89¡ f → ∀I,V,T. X = ⓕ{I}V.T →
-                         â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 f2 â\89¡ f.
+fact frees_inv_flat_aux: â\88\80f,L,X. L â\8a¢ ð\9d\90\85*â¦\83Xâ¦\84 â\89\98 f → ∀I,V,T. X = ⓕ{I}V.T →
+                         â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 f2 â\89\98 f.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #J #W #U #H destruct
 | #f #i #_ #J #W #U #H destruct
@@ -168,13 +168,13 @@ fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≡ f → ∀I,V,T. X = 
 ]
 qed-.
 
-lemma frees_inv_flat: â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\95{I}V.Tâ¦\84 â\89¡ f →
-                      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89¡ f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f2 & f1 â\8b\93 f2 â\89¡ f.
+lemma frees_inv_flat: â\88\80f,I,L,V,T. L â\8a¢ ð\9d\90\85*â¦\83â\93\95{I}V.Tâ¦\84 â\89\98 f →
+                      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85*â¦\83Vâ¦\84 â\89\98 f1 & L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f2 & f1 â\8b\93 f2 â\89\98 f.
 /2 width=4 by frees_inv_flat_aux/ qed-.
 
 (* Basic properties ********************************************************)
 
-lemma frees_eq_repl_back: â\88\80L,T. eq_repl_back â\80¦ (λf. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f).
+lemma frees_eq_repl_back: â\88\80L,T. eq_repl_back â\80¦ (λf. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f).
 #L #T #f1 #H elim H -f1 -L -T
 [ /3 width=3 by frees_sort, isid_eq_repl_back/
 | #f1 #i #Hf1 #g2 #H
@@ -195,11 +195,11 @@ lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡
 ]
 qed-.
 
-lemma frees_eq_repl_fwd: â\88\80L,T. eq_repl_fwd â\80¦ (λf. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f).
+lemma frees_eq_repl_fwd: â\88\80L,T. eq_repl_fwd â\80¦ (λf. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f).
 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
 qed-.
 
-lemma frees_lref_push: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89¡ f â\86\92 â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#⫯iâ¦\84 â\89¡ â\86\91f.
+lemma frees_lref_push: â\88\80f,i. â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#iâ¦\84 â\89\98 f â\86\92 â\8b\86 â\8a¢ ð\9d\90\85*â¦\83#â\86\91iâ¦\84 â\89\98 ⫯f.
 #f #i #H
 elim (frees_inv_atom … H) -H #g #Hg #H destruct
 /2 width=1 by frees_atom/
@@ -207,7 +207,7 @@ qed.
 
 (* Forward lemmas with test for finite colength *****************************)
 
-lemma frees_fwd_isfin: â\88\80f,L,T. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89¡ f → 𝐅⦃f⦄.
+lemma frees_fwd_isfin: â\88\80f,L,T. L â\8a¢ ð\9d\90\85*â¦\83Tâ¦\84 â\89\98 f → 𝐅⦃f⦄.
 #f #L #T #H elim H -f -L -T
 /4 width=5 by sor_isfin, isfin_isid, isfin_tl, isfin_pushs, isfin_push, isfin_next/
 qed-.