At:
l before append iff122
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] A [x; y] B (x A) & (y B)
By:
OrLeft
THEN
Using [`L2',[u; u1 / v1]]
(BackThru
Thm*L1,L2,L3:T List. L1 L2 L2 L3 L1 L3)
Generated subgoal:
[x; y] 
[u; u1 / v1]
[x; y] 
A) & (y 
L1,L2,L3:T List. L1 
L2 
