Nuprl - Proof: diagonalization 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: diagonalization 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

(

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

By:	Analyze THEN Analyze-1

Generated subgoal:

1 7. a : A
8. R((Diag f wrt x. e(x))(a),f(a,a))
False
2 steps

About:

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