T:Type, L:T List, P:(TProp). (xL.P(x))  L  {x:T| P(x) } List

By:	InductionOnList THEN RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) -1 THEN Try BackThruSomeHyp

None

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html