---

Step * of Lemma mtag_wf

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

---

Latex:


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


By

(Unfolds  ``mtag  Msg``  0  THEN  Auto)

---

Home Index