---

Step * of Lemma mk-tagged_wf

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

---

Latex:

---

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


By

---

Latex:
xxx(Unfold  `tag-case`  0  THEN  ProveWfLemma)\mcdot{}xxx

---

Home Index