Nuprl - Proof: nat descent 1 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

1. P :

Prop
2.

. P(x)

(

x':

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

x':

. x'<x

P(x')

False
5. P(x)
6. x' :

7. x'<x
8. P(x')

False

By:	FwdThru: Hyp:4 on [ x'<x ]

Generated subgoals:

None

About:

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