1 |
14. ev : {e:E| loc(e) = i Id }
15. (ev [e, e']) & (x after ev) = (x when ev) T
e ev & ev e' & (x after ev) = (x when ev) T
 | 3 steps |
2 |
14. ev : {e:E| loc(e) = i Id }
15. (ev [e, e'])
16. (x after ev) = (x when ev) T
17. e1 : E
18. e e1 & e1 e'
(x after e1) T
 | 3 steps |
3 |
14. ev : {e:E| loc(e) = i Id }
15. (ev [e, e'])
16. (x after ev) = (x when ev) T
17. e1 : E
18. e e1 & e1 e'
(x when e1) T
 | 3 steps |