Nuprl - Proof: fincr formation 1 1 1 1

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

1. P :

Prop
2.

. (

. k<j

P(k))

P(j)
3. n :

n1:

. n1<n

P(n1)

P(n)

By:	((With n (Analyze -3)) THEN (Analyze -1)) THEN Trivial

Generated subgoals:

None

About:

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