is mentioned by

Thm*  e:(BB).  Thm*  (b:B. e(b) = b) Thm*   Thm*  (A:Type, f:(AAB). (a:A. (Diag f wrt x. e(x)) = f(a)))	[diagonalization_wrt_eq]
Thm*  R:(BBProp), e:(BB). Thm*  (b:B. R(e(b),b)) Thm*   Thm*  (A:Type, f:(AAB). (a:A. R((Diag f wrt x. e(x))(a),f(a,a))))	[diagonalization]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html