(6steps total) PrintForm Definitions PrimesSquareRoots Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There is no inhabited class of natural numbers in which one can always find a smaller member.

At: nat descent

  P:(Prop). (x:. P(x)  (x':. x'<x & P(x')))  (x:. P(x))
By: Auto

Generated subgoal:

1 1. P : Prop
2. x:. P(x)  (x':. x'<x & P(x'))
  (x:. P(x))
5 steps

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

(6steps total) PrintForm Definitions PrimesSquareRoots Sections DiscrMathExt Doc