At:
sublist append iff12211
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.
u2: T
12.
v2: T List
13.
B': T List
14.
[u / v] = [u2 / (v2 @ B')]
15.
u2 = u1
16.
v2 v1
17.
B' B
u = u1
By:
ObviousFrom [-4;-3]
Generated subgoals:
A,B:T List. v 
A @ B 
(
A',B':T List. v = (A' @ B') & A' 
u = u1