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

1	1. T: Type 2. L: T List x,y:T. x before y nil (L1,L2,L3:T List. nil = (L1 @ [x] @ L2 @ [y] @ L3))	1 step
2	1. T: Type 2. L: T List 3. u: T 4. v: T List 5. 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))	12 steps

About: