Nuprl - Proof: rel rel star 1

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

1. T : Type
2. R : T

Prop
3. x : T
4. y : T
5. x R y

x (R^*) y

By:	Unfold `rel_star` 0 THEN Reduce 0 THEN InstConcl [1]

Generated subgoal:

1 x R^1 y
1 step

About:

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