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