At:
l before decomp1221
1.
T: Type
2.
L: T List
3.
u: T
4.
v: T List
5.
x,y:T. [x; y] v (A,B:T List. v = (A @ B) & (x A) & (y B))
6.
x: T
7.
y: T
8.
[x; y] v
9.
A: T List
10.
B: T List
11.
v = (A @ B)
12.
(x A)
13.
(y B)
[u / v] = [u / (A @ B)]
By:
Analyze
Generated subgoals:
x,y:T. [x; y] 
v 
(
A,B:T List. v = (A @ B) & (x 
A) & (y 
[u / v] = [u / (A @ B)]