x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x] @ L2 @ [y] @ L3))

x,y:T. x before y [u / v] (L1,L2,L3:T List. [u / v] = (L1 @ [x] @ L2 @ [y] @ L3))

1

6. x: T 7. y: T x before y [u / v] (L1,L2,L3:T List. [u / v] = (L1 @ [x] @ L2 @ [y] @ L3))

11 steps

About: