Nuprl - Proof: all-nsub-add1 1

1. n:
2. P: (n+1)Prop
3. P(0)
4. x:n. P(x+1)
5. x: (n+1)
6. x = 0

P(x)

By: InstHyp [x-1] -3 THEN NthHypSq -1 THEN Analyze THEN Try Trivial

Generated subgoal:

1 7. P(x-1+1)
x ~ (x-1+1) 1 step

About: