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)) ~ (i:{a:}B(i))

By:	OOCifExteq THEN Try BackThru: Thm*  a,a':. a'-a = 1  ({a..a'} =ext {a:})

1

(i:{a..a'}B(i)) =ext (i:{a:}B(i))

1 step

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