At:
l before-iff21111
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
8.
x = u
9.
(y v)
10.
s1: T List
11.
s2: T List
12.
v = (s1 @ [y / s2])
[u / v] = [x / (s1 @ [y / s2])]
By:
Analyze
Generated subgoals:
x,y:T. x before y 
v 
(
L1,L2,L3:T List. v = (L1 @ [x] @ L2 @ [y] @ L3))
[u / v] = [x / (s1 @ [y / s2])]