X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_fqup.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Ffrees_fqup.ma;h=fab29bbe6d24a1099168a3de314e9e7830b5bf55;hb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;hp=8946c6e4a2f59636a34f1c9f2aa9068cb706af1c;hpb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;p=helm.git

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 8946c6e4a..fab29bbe6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
@@ -70,7 +70,7 @@ elim (pn_split f2) * #g2 #H destruct
   lapply (sor_comm … Hz) -Hz #Hz
   lapply (sor_mono … f Hz ?) // -Hz #H
   lapply (sor_inv_sle_sn … Hf) -Hf #Hf
-  lapply (frees_eq_repl_back … Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
+  lapply (frees_eq_repl_back … Hf0 (↑f) ?) /2 width=5 by eq_next/ -z #Hf0
   @(frees_bind … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
   /2 width=1 by sor_sle_dx/
 ]
@@ -104,15 +104,15 @@ lemma frees_ind_void: ∀R:relation3 ….
                       (
                          ∀f,L,s. 𝐈⦃f⦄ → R L (⋆s) f
                       ) → (
-                         ∀f,i. 𝐈⦃f⦄ → R (⋆) (#i) (↑*[i]⫯f)
+                         ∀f,i. 𝐈⦃f⦄ → R (⋆) (#i) (⫯*[i]↑f)
                       ) → (
                          ∀f,I,L,V.
-                         L ⊢ 𝐅*⦃V⦄ ≘ f → R L V f→ R (L.ⓑ{I}V) (#O) (⫯f) 
+                         L ⊢ 𝐅*⦃V⦄ ≘ f → R L V f→ R (L.ⓑ{I}V) (#O) (↑f) 
                       ) → (
-                         ∀f,I,L. 𝐈⦃f⦄ → R (L.ⓤ{I}) (#O) (⫯f)
+                         ∀f,I,L. 𝐈⦃f⦄ → R (L.ⓤ{I}) (#O) (↑f)
                       ) → (
                          ∀f,I,L,i.
-                         L ⊢ 𝐅*⦃#i⦄ ≘ f → R L (#i) f → R (L.ⓘ{I}) (#(⫯i)) (↑f)
+                         L ⊢ 𝐅*⦃#i⦄ ≘ f → R L (#i) f → R (L.ⓘ{I}) (#(↑i)) (⫯f)
                       ) → (
                          ∀f,L,l. 𝐈⦃f⦄ → R L (§l) f
                       ) → (