update in ground, basic_2A and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / functional / mf.ma

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
index 4e88c1a78568e2e448153325766172bd78596455..3d5d22b6467905e36ee778af350e6b5b16c73de8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
@@ -35,19 +35,19 @@ interpretation "term filling (multiple filling)"
 
 (* Basic Properties *********************************************************)
 
-lemma mf_sort: â\88\80gv,lv,s. â\97\8f[gv,lv]⋆s = ⋆s.
+lemma mf_sort: â\88\80gv,lv,s. â\96 [gv,lv]⋆s = ⋆s.
 // qed.
 
-lemma mf_lref: â\88\80gv,lv,i. â\97\8f[gv,lv]#i = lv i.
+lemma mf_lref: â\88\80gv,lv,i. â\96 [gv,lv]#i = lv i.
 // qed.
 
-lemma mf_gref: â\88\80gv,lv,l. â\97\8f[gv,lv]§l = gv l.
+lemma mf_gref: â\88\80gv,lv,l. â\96 [gv,lv]§l = gv l.
 // qed.
 
 lemma mf_bind (p) (I): ∀gv,lv,V,T.
-                       â\97\8f[gv,lv]â\93\91[p,I]V.T = â\93\91[p,I]â\97\8f[gv,lv]V.â\97\8f[⇡[0]gv,⇡[0←#0]lv]T.
+                       â\96 [gv,lv]â\93\91[p,I]V.T = â\93\91[p,I]â\96 [gv,lv]V.â\96 [⇡[0]gv,⇡[0←#0]lv]T.
 // qed.
 
 lemma mf_flat (I): ∀gv,lv,V,T.
-                   â\97\8f[gv,lv]â\93\95[I]V.T = â\93\95[I]â\97\8f[gv,lv]V.â\97\8f[gv,lv]T.
+                   â\96 [gv,lv]â\93\95[I]V.T = â\93\95[I]â\96 [gv,lv]V.â\96 [gv,lv]T.
 // qed.