Step
*
of Lemma
decidable__nameset
∀L:Cname List. ∀a:Cname. Dec(a ∈ nameset(L))
BY
{ (UnivCD THENA Auto) }
1
1. L : Cname List
2. a : Cname
⊢ Dec(a ∈ nameset(L))
Latex:
Latex:
\mforall{}L:Cname List. \mforall{}a:Cname. Dec(a \mmember{} nameset(L))
By
Latex:
(UnivCD THENA Auto)
Home
Index