---

Step * of Lemma msg_wf

∀[M:IdLnk ⟶ Id ⟶ Type]. ∀[l:IdLnk]. ∀[t:Id]. ∀[v:M l t].  (msg(l;t;v) ∈ Msg(M))
BY
{ (Unfolds ``msg Msg`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[M:IdLnk  {}\mrightarrow{}  Id  {}\mrightarrow{}  Type].  \mforall{}[l:IdLnk].  \mforall{}[t:Id].  \mforall{}[v:M  l  t].    (msg(l;t;v)  \mmember{}  Msg(M))


By

---

Latex:
(Unfolds  ``msg  Msg``  0  THEN  Auto)

---

Home Index