Nuprl - Proof: nat well founded 1

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

P:(

Prop). (

. (

. k<j

P(k))

P(j))

(

. P(n))

By:

RepD

Generated subgoal:

1 1. P : Prop
2. j:. (k:. k<j P(k)) P(j)
n:. P(n)
2 steps

About:

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