update in ground_2, static_2, basic_2, apps_2, alpha_1

[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 6f2074db5b290e2d75b65b42607988c18c4eb16f..4e88c1a78568e2e448153325766172bd78596455 100644 (file)
--- 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.