---

Step * of Lemma member-of-tagged+2

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index