(6steps total) PrintForm Definitions PrimesSquareRoots Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat descent 1 1 1
1. P : Prop
2. x:. P(x)  (x':. x'<x & P(x'))
3. x : 
4. x':. x'<x  P(x')  False
  P(x)  False
By: Analyze THEN FwdThru: Hyp:2 on [ Hyp:5 ]

Generated subgoal:

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

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

(6steps total) PrintForm Definitions PrimesSquareRoots Sections DiscrMathExt Doc