Nuprl - DiscreteMath LEMMAs for no_finite

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

Rank	Theorem	Name
4	Thm* (A:Type, R:(AAProp). Thm* ((A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm* (& (x:A. R(x;x)) Thm* (& Finite(A))	[no_finite_model]
cites the following:
0	Thm* R:(AAProp). Thm* (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm* Thm* (k:. f:(kA). i,j:k. i<j R(f(i);f(j)))	[no_finite_model_lemma]
3	Thm* m,k:, f:(mk). k<m (x,y:m. x y & f(x) = f(y))	[pigeon_hole]

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