1. T : Type
2. P : TProp
3. x:T. Dec(P(x))
4. L : T List
5. x:T. P(x)  (x  L)
  L:T List. x:T. P(x)  (x  L)

By:	Assert (f:(T). x:T. f(x)  P(x))

1	f:(T). x:T. f(x)  P(x)	3 steps
2	6. f:(T). x:T. f(x)  P(x)   L:T List. x:T. P(x)  (x  L)	1 step

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