---

Step * of Lemma mk-tagged_wf_unequal

∀[B:Type]. ∀[tg,a:Atom].  ∀[x:Top]. (mk-tagged(a;x) ∈ tg:B) supposing ¬(tg = a ∈ Atom)
BY
{ xxx(Unfold `tag-case` 0 THEN ProveWfLemma THEN AutoSplit)xxx }

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[tg,a:Atom].    \mforall{}[x:Top].  (mk-tagged(a;x)  \mmember{}  tg:B)  supposing  \mneg{}(tg  =  a)


By

---

Latex:
xxx(Unfold  `tag-case`  0  THEN  ProveWfLemma  THEN  AutoSplit)xxx

---

Home Index