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

1

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

3 steps

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