B:Type, e:(BB).
  (b:B. e(b) = b)
  
  (A:Type, f:(AAB). (a:A. (Diag f wrt x. e(x)) = f(a)))

By:	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)))) ; Auto

1

1. B : Type 2. e : BB 3. b:B. e(b) = b 4. A : Type 5. f : AAB   (a:A. (Diag f wrt x. e(x)) = f(a))

3 steps

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