(* 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.