At:
l before-iff21
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))
6.
x: T
7.
y: T
x before y [u / v] (L1,L2,L3:T List. [u / v] = (L1 @ [x] @ L2 @ [y] @ L3))
By:
RWO
Thm*l:T List, a,x,y:T. x before y [a / l] x = a & (y l) x before y l
0
Generated subgoals: