Nuprl - Proof: rel star finite 2

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

1. n :

2. R :

Prop
3. x :

n
4. y :

n
5.

(n+1). x R^k y

x (R^*) y

By:	Unfold `rel_star` 0 THEN Reduce 0 THEN ParallelOp -1

Generated subgoals:

None

About:

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