---

Step * of Lemma member-of-tagged+1

∀[T,B:Type]. ∀[tg,a:Atom]. ∀[x:T].  mk-tagged(tg;x) ∈ tg:T |+ a:B supposing ¬(tg = a ∈ Atom)
BY
{ Auto }

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index