(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. n:. ( ~ n)  ( ~ (n+1))
2. n : 
3.  ~ n
  False
By: FwdThru: Hyp:1 on [  ~ n ]

Generated subgoal:

1 4.  ~ (n+1)
  False
2 steps

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