P:(Prop), a:.
  (b:{...a}. P(a,b))
  
  ((b:{...a}. P(a,b))  (b:{a...}. P(a,b)))  (b:. P(a,b))

1

1. P : Prop 2. a :  3. b:{...a}. P(a,b) 4. (b:{...a}. P(a,b))  (b:{a...}. P(a,b)) 5. b :    P(a,b)

3 steps

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