Nuprl - Proof: preserved by star 1 1 2 1

(8steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: preserved by star 1 1 2 1

1. T : Type
2. P : T

Prop
3. R : T

T

Prop
4.

x,y:T. P(x)

(x R y)

P(y)
5. n :

6. 0<n
7. n-1

0

(

x,y:T. P(x)

(x R^n-1 y)

P(y))
8. n

0
9. x : T
10. y : T
11. P(x)
12.

n = 0
13.

z:T. (x R z) & (z R^n-1 y)

P(y)

By:

ExRepD

Generated subgoal:

1 13. z : T
14. x R z
15. z R^n-1 y
P(y)
2 steps

About:

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

(8steps total) PrintForm Definitions mb nat Sections MarkB generic Doc