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

By:	OOCinterpolate (i:{a:}B(i)) THENW (Auto THEN BackThru: Thm*  a,a':. a'-a = 1  ({a..a'} =ext {a:}))

1	(i:{a..a'}B(i)) ~ (i:{a:}B(i))	2 steps
2	(i:{a:}B(i)) ~ B(a)	1 step

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