update in ground and static_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
index 887703487aaaef9bbee50c968015d91d306ccf71..e9e6380d408e8c8dc5de8ffdfbc4c41876ddc769 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
@@ -28,7 +28,7 @@ inductive frees: relation3 lenv term rtmap ≝
               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 â\8b\93 ⫱f2 ≘ f → frees L (ⓑ[p,I]V.T) f
+              f1 â\8b\93 â«°f2 ≘ 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 ⋓ f2 ≘ f → frees L (ⓕ[I]V.T) f
 .
@@ -143,7 +143,7 @@ lemma frees_inv_gref: ∀f,L,l. L ⊢ 𝐅+❪§l❫ ≘ f → 𝐈❪f❫.
 
 fact frees_inv_bind_aux:
      ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
-     â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+     â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #q #J #W #U #H destruct
 | #f #i #_ #q #J #W #U #H destruct
@@ -158,7 +158,7 @@ qed-.
 
 lemma frees_inv_bind:
       ∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
-      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 ⫱f2 ≘ f.
+      â\88\83â\88\83f1,f2. L â\8a¢ ð\9d\90\85+â\9dªVâ\9d« â\89\98 f1 & L.â\93\91[I]V â\8a¢ ð\9d\90\85+â\9dªTâ\9d« â\89\98 f2 & f1 â\8b\93 â«°f2 ≘ f.
 /2 width=4 by frees_inv_bind_aux/ qed-.
 
 fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,V,T. X = ⓕ[I]V.T →