At:
sublist append iff1222
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 / v2] v1
16.
B' B
u = u1 & v v1 @ B [u / v] v1 @ B
By:
OrRight
THEN
RW (HypC 9) 0
THEN
InstConcl [[u2 / v2];B']
THEN
Reduce 0
Generated subgoals:
A,B:T List. v 
A @ B 
(
A',B':T List. v = (A' @ B') & A' 
u = u1 & v 
[u / v]