Nuprl - Proof: no finite model

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

(

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:

Generated subgoal:

1 1. A : Type
2. R : AAProp
3. A
4. Trans x,y:A. R(x;y)
5. x:A. y:A. R(x;y)
6. Finite(A)
x:A. R(x;x)
16 steps

About:

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