Nuprl - Proof: nat descent 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat descent 1 1

1. P :

Prop
2.

. P(x)

(

x':

. x'<x & P(x'))
3. x :

4. P(x)

False

By:	CompNatInd Hyp:3 THEN CBV4: x'

Generated subgoal:

1 4. x':. x'<x P(x') False
P(x) False
3 steps

About:

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