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

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

None

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