(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There are as many non-negative integers as integers.

At: int ooc nat

   ~ 
By: BackThru: Thm*  (f:(AB). Bij(A; B; f))  (A ~ B)

Generated subgoal:

1   f:(). Bij(; ; f)
26 steps

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

(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc