||tr||8. y:
||tr||9. x switchR(tr) y
is-send(E)(tr[x])
x,y:||tr||. (x (switchR(tr)^*) y) 
is-send(E)(tr[x]) 
x = y is-send(E)(tr[i])||tr||||tr|| is-send(E)(tr[i])R,R2:(T
TProp).
Trans(T)(R2(_1,_2)) (x,y:T. (x R y) (x R2 y)) (x,y:T. (x (R^*) y) (x R2 y) x = y)
[||tr||;switchR(tr);
i,j. is-send(E)(tr[i])]
| 1 | 7. x: ||tr|| 8. y: ||tr||9. x switchR(tr) y is-send(E)(tr[x]) |
| 2 | 7. x,y:||tr||. (x (switchR(tr)^*) y) is-send(E)(tr[x]) x = y is-send(E)(tr[i]) |
About:
 |  |  |  |  |