---

Step * of Lemma mk-tagged_wf2

∀[B:Type]. ∀[tg:Atom]. ∀[x:B].  (mk-tagged(tg;x) ∈ tg×B)
BY
{ (Unfold `tag-by` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[tg:Atom].  \mforall{}[x:B].    (mk-tagged(tg;x)  \mmember{}  tg\mtimes{}B)


By

---

Latex:
(Unfold  `tag-by`  0  THEN  ProveWfLemma)

---

Home Index