A:Type, x:A. (x,y:A. Dec(x = y))  (L:A List. Dec((x  L)))

By:	InductionOnList THEN Try (RWO Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0) THEN Try (RWO Thm* x:T. (x  nil)  False 0)

None

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