---

Step * of Lemma mval_wf

∀[M:IdLnk ⟶ Id ⟶ Type]. ∀[m:Msg(M)].  (mval(m) ∈ M mlnk(m) mtag(m))
BY
{ (Unfolds ``mval mlnk mtag Msg`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type].  \mforall{}[m:Msg(M)].    (mval(m)  \mmember{}  M  mlnk(m)  mtag(m))


By

---

Latex:
(Unfolds  ``mval  mlnk  mtag  Msg``  0  THEN  Auto)

---

Home Index