(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 2 1 1
1. n:. ( ~ n)  ( ~ (n+1))
2. n : 
3.  ~ n
4.  ~ (n+1)
  False
By: Rewrite-1 by  ~ n

Generated subgoal:

1 5. n ~ (n+1)
  False
1 step

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

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