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

By:	Guarding (b:{a...}. P(a,b)) Auto

1

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

6 steps

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