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

By:	Auto THEN Inst Thm* L:T List. L  {x:T| (x  L) } List [T;L] THEN DoSubsume THEN UseSubtypeRelLemmas

1

1. T : Type 2. L : T List 3. P : TProp 4. (xL.P(x)) 5. L  {x:T| (x  L) } List   {x:T| (x  L) } r {x:T| P(x) }

2 steps

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