(7steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The infinite sequences of numbers cannot be paired one-to-one with the numbers themselves. (Cantor)

At: not nat occ natfuns

  (() ~ )
By: Analyze

Generated subgoal:

1 1. () ~ 
  False
6 steps

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

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