Nuprl - Proof: rel inverse star 2

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

1. T : Type
2. R : T

Prop
3. x : T
4. y : T
5. x (R^-1^*) y

x R^*^-1 y

By:	Unfold `rel_star` -1 THEN Unfold `rel_inverse` 0 THEN Unfold `rel_star` 0 THEN All Reduce

Generated subgoal:

1 5. n:. x R^-1^n y
n:. y R^n x
2 steps

About:

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