---

Step * of Lemma member-tagged+-right

∀[T,B:Type]. ∀[a:Atom]. ∀[p:T |+ a:B].  p ∈ T supposing ¬(p.tag = a ∈ Atom)
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[T,B:Type].  \mforall{}[a:Atom].  \mforall{}[p:T  |+  a:B].    p  \mmember{}  T  supposing  \mneg{}(p.tag  =  a)


By

---

Latex:
Auto

---

Home Index