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

1

4. L : T List 5. x:T. P(x)  (x  L)   L:T List. x:T. P(x)  (x  L)

5 steps

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