T:Type, l:T List, P:(T), x,y:T.
  x before y  filter(P;l)  P(x) & P(y) & x before y  l

By:	Unfold `l_before` 0 THEN UnivCD THEN RWO Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x)) 0 THEN RWW Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) 0 THEN Easy

None

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