At:
l before decomp121
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 = u & [y] v A,B:T List. [u / v] = (A @ B) & (x A) & (y B)
By:
InstConcl [[u];v]
THEN
Reduce 0
Generated subgoals: