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))

By:	Inst:  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)))) Using:[B | R(x,y):= x = y  B | e | A | f]

1

6. (a:A. (Diag f wrt x. e(x))(a) = f(a,a))   (a:A. (Diag f wrt x. e(x)) = f(a))

2 steps

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