Nuprl - Proof: rel inverse star

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

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

T:Type, R:(T

Prop), x,y:T. (x R^*^-1 y)

(x (R^-1^*) y)

By:

Auto

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. x : T
4. y : T
5. x R^*^-1 y
x (R^-1^*) y
3 steps

2 1. T : Type
2. R : TTProp
3. x : T
4. y : T
5. x (R^-1^*) y
x R^*^-1 y
3 steps

About:

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

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

1	1. T : Type 2. R : TTProp 3. x : T 4. y : T 5. x R^^-1 y x (R^-1^) y	3 steps
2	1. T : Type 2. R : TTProp 3. x : T 4. y : T 5. x (R^-1^) y x R^^-1 y	3 steps