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

1

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

1 step

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