At:
sublist append iff1121
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.
A': T List
12.
B': T List
13.
A' v1
A' [u1 / v1]
By:
Analyze -3
THEN
ObviousFrom [-1]
Generated subgoals:
A,B:T List. v 
A @ B 
(
A',B':T List. v = (A' @ B') & A' 
A'