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