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