Nuprl - Proof: no finite model a

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: no finite model a

(

A:Type, R:(A

Prop).

((

A) & (Trans x,y:A. R(x;y)) & (

x:A.

y:A. R(x;y))

(

x:A. R(x;x))

(& Finite(A))

By:

Analyze

Generated subgoal:

1 1. A:Type, R:(AAProp).
1. (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y))
1. & (x:A. R(x;x))
1. & Finite(A)
False
3 steps

About:

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