Def  Finite(A) == n:. A ~ n

is mentioned by

Thm*  Dedekind-Infinite(A)  Finite(A)	[dedekind_imp_nonfin]
Thm*  Finite()	[nat_not_finite]
Thm*  (A:Type. Finite(A)  Infinite(A))  (D:Type. (D)  (D))	[absurd_nonfinite_imp_infinite]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (P:Prop. P  P)	[nonfin_eqv_unb_inf_iff_negnegelim]
Thm*  (A:Type. Finite(A)  Unbounded(A))  (D:Type. (D)  (D))	[absurd_nonfin_imp_unb_inf]
Thm*  (P:Prop. P  P)  (A:Type. Finite(A)  Unbounded(A))	[negnegelim_imp_notfin_imp_unb_inf]
Thm*  Infinite(A)  Finite(A)	[infinite_imp_nonfinite]
Thm*  Unbounded(A)  Finite(A)	[unb_inf_not_fin]
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]
Thm*  (A ~ B)  Finite(A)  Finite(B)	[ooc_preserves_finiteness]
Thm*  k:. Finite(k)	[nsub_is_finite]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html