(12steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat not finite 1 1
1. n : 
2.  ~ n
   ~ (n+1)
By: ExistHD Hyp:-1

Generated subgoal:

1 2. f : n
3. g : n
4. InvFuns(;n;f;g)
   ~ (n+1)
5 steps

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

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