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