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

By:	b:{a...}. P(a,b)  Asserted

1	b:{a...}. P(a,b)	7 steps
2	5. b:{a...}. P(a,b) 6. b :    P(a,b)	3 steps

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