X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees.ma;h=b35ea99b828235e63e509e378d657cf5802ce5ed;hp=12cf981878148a7cef3e2433b4065645cd648ea1;hb=222044da28742b24584549ba86b1805a87def070;hpb=75f395f0febd02de8e0f881d918a8812b1425c8d

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
index 12cf98187..b35ea99b8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
@@ -20,12 +20,12 @@ include "basic_2/syntax/lenv.ma".
 
 inductive frees: relation3 lenv term rtmap ≝
 | frees_sort: ∀f,L,s. 𝐈⦃f⦄ → frees L (⋆s) f
-| frees_atom: ∀f,i. 𝐈⦃f⦄ → frees (⋆) (#i) (↑*[i]⫯f)
+| frees_atom: ∀f,i. 𝐈⦃f⦄ → frees (⋆) (#i) (⫯*[i]↑f)
 | frees_pair: ∀f,I,L,V. frees L V f →
-              frees (L.ⓑ{I}V) (#0) (⫯f)
-| frees_unit: ∀f,I,L. 𝐈⦃f⦄ → frees (L.ⓤ{I}) (#0) (⫯f)
+              frees (L.ⓑ{I}V) (#0) (↑f)
+| frees_unit: ∀f,I,L. 𝐈⦃f⦄ → frees (L.ⓤ{I}) (#0) (↑f)
 | frees_lref: ∀f,I,L,i. frees L (#i) f →
-              frees (L.ⓘ{I}) (#⫯i) (↑f)
+              frees (L.ⓘ{I}) (#↑i) (⫯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 ⋓ ⫱f2 ≘ f → frees L (ⓑ{p,I}V.T) f
@@ -54,7 +54,7 @@ lemma frees_inv_sort: ∀f,L,s. L ⊢ 𝐅*⦃⋆s⦄ ≘ f → 𝐈⦃f⦄.
 /2 width=5 by frees_inv_sort_aux/ qed-.
 
 fact frees_inv_atom_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀i. L = ⋆ → X = #i →
-                         ∃∃g. 𝐈⦃g⦄ & f = ↑*[i]⫯g.
+                         ∃∃g. 𝐈⦃g⦄ & f = ⫯*[i]↑g.
 #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: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≘ f → ∃∃g. 𝐈⦃g⦄ & f = ↑*[i]⫯g.
+lemma frees_inv_atom: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≘ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯*[i]↑g.
 /2 width=5 by frees_inv_atom_aux/ qed-.
 
 fact frees_inv_pair_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀I,K,V. L = K.ⓑ{I}V → X = #0 →
-                         ∃∃g. K ⊢ 𝐅*⦃V⦄ ≘ g & f = ⫯g.
+                         ∃∃g. K ⊢ 𝐅*⦃V⦄ ≘ g & f = ↑g.
 #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: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≘ f → ∃∃g. K ⊢ 𝐅*⦃V⦄ ≘ g & f = ⫯g.
+lemma frees_inv_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≘ f → ∃∃g. K ⊢ 𝐅*⦃V⦄ ≘ g & f = ↑g.
 /2 width=6 by frees_inv_pair_aux/ qed-.
 
 fact frees_inv_unit_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀I,K. L = K.ⓤ{I} → X = #0 →
-                         ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
+                         ∃∃g. 𝐈⦃g⦄ & f = ↑g.
 #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: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≘ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g.
+lemma frees_inv_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≘ f → ∃∃g. 𝐈⦃g⦄ & f = ↑g.
 /2 width=7 by frees_inv_unit_aux/ qed-.
 
-fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀I,K,j. L = K.ⓘ{I} → X = #(⫯j) →
-                         ∃∃g. K ⊢ 𝐅*⦃#j⦄ ≘ g & f = ↑g.
+fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀I,K,j. L = K.ⓘ{I} → X = #(↑j) →
+                         ∃∃g. K ⊢ 𝐅*⦃#j⦄ ≘ 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,8 +118,8 @@ fact frees_inv_lref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀I,K,j. L = K.
 ]
 qed-.
 
-lemma frees_inv_lref: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≘ f →
-                      ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≘ g & f = ↑g.
+lemma frees_inv_lref: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(↑i)⦄ ≘ f →
+                      ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≘ g & f = ⫯g.
 /2 width=6 by frees_inv_lref_aux/ qed-.
 
 fact frees_inv_gref_aux: ∀f,L,X. L ⊢ 𝐅*⦃X⦄ ≘ f → ∀x. X = §x → 𝐈⦃f⦄.
@@ -199,7 +199,7 @@ lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≘ f)
 #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/
 qed-.
 
-lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≘ f → ⋆ ⊢ 𝐅*⦃#⫯i⦄ ≘ ↑f.
+lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≘ f → ⋆ ⊢ 𝐅*⦃#↑i⦄ ≘ ⫯f.
 #f #i #H
 elim (frees_inv_atom … H) -H #g #Hg #H destruct
 /2 width=1 by frees_atom/