Nuprl - Proof: diagonalization 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: diagonalization 1 1

1. B : Type
2. R : B

Prop
3. e : B

B
4.

b:B.

R(e(b),b)
5. A : Type
6. f : A

B
7. a : A
8. R((Diag f wrt x. e(x))(a),f(a,a))

False

By:	(-1) Def of Diag f wrt x. e(x) THEN Reduce Hyp:-1

Generated subgoal:

1 8. R(e(f(a,a)),f(a,a))
False
1 step

About:

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