Nuprl - Proof: diagonalization 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: diagonalization 1 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(e(f(a,a)),f(a,a))

False

By:	BackThru: Hyp:4 Using:[f(a,a)]

Generated subgoals:

None

About:

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