a,a':. a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a)))

1

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

2 steps

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