P:(Prop). (i:. (j:i. P(j))  P(i))  (i:. P(i))

1

1. P : Prop 2. i:. (j:i. P(j))  P(i) 3. i :    P(i)

2 steps

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