1. a : 
2. a' : 
3. a'-a = 1
4. B : {a..a'}Type
  (i:{a..a'}B(i)) =ext ({a:}B(a))

By:	Analyze THEN Analyze THEN New:[i | b] Analyze-1 THEN Analyze THEN Try BackThru: Thm*  a,a':. a'-a = 1  ({a..a'} =ext {a:})

1	5. i : {a..a'} 6. b : B(i)   b  B(a)	2 steps
2	5. i : {a:} 6. b : B(a)   b  B(i)	3 steps

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