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

By:	Rewrite by ({a:}B(a)) ~ B(a) THEN Repeat BackThru:  Thm*  B:({a:A}Type). (i:{a:A}B(i)) ~ B(a) | Thm*  a,a':. Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a)))

None

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