Nuprl - Proof: nat descent 1 1 1 1

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

1. P :

Prop
2.

. P(x)

(

x':

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

x':

. x'<x

P(x')

False
5. P(x)
6.

x':

. x'<x & P(x')

False

By:	ExistHD Hyp:6

Generated subgoal:

1 6. x' :
7. x'<x
8. P(x')
False
1 step

About:

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