1. A : Type
2. B : AType
3. f : d:A Lista:{a:A| (a  d) }B(a)
4. eq : EqDecider(A)
5. x : A
6. deq-member(eq;x;1of(f))
  x  {a:A| (a  1of(f)) }

By:	RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) -1 THEN Analyze

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html