IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
trans imp sp trans b T:Type, R:(TTProp).
(Trans a,b:T. R(a,b))
(a,b,c:T.
(strict_part(x,y.R(x,y);a;b) R(b,c) strict_part(x,y.R(x,y);a;c))
By:
Unfolds [`trans`;`strict_part`;`guard`] 0 THEN GenRepD