e:(B
B).
Thm* (
b:B. 
e(b) = b)
Thm*
Thm* (
A:Type, f:(AAB). (
a:A. (Diag f wrt x. e(x)) = f(a)))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))))| Theorem | Name |
| e:(BB).
Thm* ( b:B. e(b) = b)
Thm*
Thm* ( A:Type, f:(AAB). (a:A. (Diag f wrt x. e(x)) = f(a))) | [diagonalization_wrt_eq] |
| cites the following: | |
| 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)))) | [diagonalization] |