IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
diagonalization wrt eq111 1. B : Type
2. e : BB 3. b:B. e(b) = b 4. A : Type
5. f : AAB 6. a : A 7. (Diag f wrt x. e(x)) = f(a)
(Diag f wrt x. e(x))(a) = f(a,a)
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B
b:B. 
e(b) = b
(Diag f wrt x. e(x))(a) = f(a,a)
