---

Step * of Lemma tagged-tag_wf2

∀[T,B:Type]. ∀[z:Atom]. ∀[x:T |+ z:B].  (x.tag ∈ Atom)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T,B:Type].  \mforall{}[z:Atom].  \mforall{}[x:T  |+  z:B].    (x.tag  \mmember{}  Atom)


By

---

Latex:
ProveWfLemma

---

Home Index