At:
l before append iff1221
1.
T: Type
2.
A: T List
3.
B: T List
4.
x: T
5.
y: T
6.
u: T
7.
u1: T
8.
v1: T List
9.
B': T List
10.
[x; y] = [u; u1 / (v1 @ B')]
11.
[u; u1 / v1] A
12.
B' B
[x; y] [u; u1 / v1]
By:
RWO
Thm*x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2
0
THEN
OrLeft
THEN
Try Obvious
THEN
RWO
Thm*x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2
0
THEN
OrLeft
THEN
Thin -1
THEN
Try Obvious
Generated subgoals:
A
[x; y] 
x1,x2:T, L1,L2:T List. [x1 / L1] 
x1 = x2 & L1 
[x1 / L1]