IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
no finite model lemma11 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. k : 7. 0<k 8. 1 = k f:(kA). i,j:k. i<jR(f(i);f(j))
By:
Rename3: a THEN Witness: z.a
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A
A
x:A. 
k
R(f(i);f(j))
z.a
