T:Type, P:(T), l:T List. no_repeats(T;l)  no_repeats(T;filter(P;l))

By:	((RWO Thm* l:T List. no_repeats(T;l)  (x,y:T. x before y  l  x = y) 0) (THEN ((RWO ((Thm* l:T List, P:(T), x,y:T. ((Thm* x before y  filter(P;l)  P(x) & P(y) & x before y  l ((0)) THEN BackThruSomeHyp

None

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