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

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma
index 4e88c1a78..3d5d22b64 100644
--- 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: ∀gv,lv,s. ●[gv,lv]⋆s = ⋆s.
+lemma mf_sort: ∀gv,lv,s. ■[gv,lv]⋆s = ⋆s.
 // qed.
 
-lemma mf_lref: ∀gv,lv,i. ●[gv,lv]#i = lv i.
+lemma mf_lref: ∀gv,lv,i. ■[gv,lv]#i = lv i.
 // qed.
 
-lemma mf_gref: ∀gv,lv,l. ●[gv,lv]§l = gv l.
+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.