X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Fmf.ma;h=4e88c1a78568e2e448153325766172bd78596455;hp=6f2074db5b290e2d75b65b42607988c18c4eb16f;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
index 6f2074db5..4e88c1a78 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
@@ -45,9 +45,9 @@ lemma mf_gref: ∀gv,lv,l. ●[gv,lv]§l = gv l.
 // qed.
 
 lemma mf_bind (p) (I): ∀gv,lv,V,T.
-                       ●[gv,lv]ⓑ{p,I}V.T = ⓑ{p,I}●[gv,lv]V.●[⇡[0]gv,⇡[0←#0]lv]T.
+                       ●[gv,lv]ⓑ[p,I]V.T = ⓑ[p,I]●[gv,lv]V.●[⇡[0]gv,⇡[0←#0]lv]T.
 // qed.
 
 lemma mf_flat (I): ∀gv,lv,V,T.
-                   ●[gv,lv]ⓕ{I}V.T = ⓕ{I}●[gv,lv]V.●[gv,lv]T.
+                   ●[gv,lv]ⓕ[I]V.T = ⓕ[I]●[gv,lv]V.●[gv,lv]T.
 // qed.