Nuprl - Proof: rel star finite 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star finite 1

1. n :

2. R :

Prop
3. x :

n
4. y :

n
5. x (R^*) y

(n+1). x R^k y

By:	Unfold `rel_star` -1 THEN Reduce -1 THEN ExRepD

Generated subgoal:

1 5. n@0 :
6. x R^n@0 y
k:(n+1). x R^k y
38 steps

About:

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