(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
1. n:. ( ~ n)  ( ~ (n+1))
2. n : 
3.  ~ n
4.  ~ (n+1)
5. n ~ (n+1)
  False
By: FwdThru: Thm*  a,b:. (a ~ b)  a = b on [ n ~ (n+1) ]

Generated subgoals:

None

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

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