At:
sublist append iff1111
1.
T: Type
2.
C: T List
3.
u: T
4.
v: T List
5.
A,B:T List. v A @ B (A',B':T List. v = (A' @ B') & A' A & B' B)
6.
A: T List
7.
u1: T
8.
v1: T List
9.
B:T List. [u / v] v1 @ B (A',B':T List. [u / v] = (A' @ B') & A' v1 & B' B)
10.
B: T List
11.
u = u1
12.
A': T List
13.
B': T List
14.
v = (A' @ B')
15.
A' v1
16.
B' B
[u / v] = [u / (A' @ B')]
By:
Analyze
Generated subgoals:
A,B:T List. v 
A @ B 
(
A',B':T List. v = (A' @ B') & A' 
[u / v] = [u / (A' @ B')]