At:
l before append iff121
1.
T: Type
2.
A: T List
3.
B: T List
4.
x: T
5.
y: T
6.
u: T
7.
B': T List
8.
[x; y] = [u / B']
9.
[u] A
10.
B' B
[x; y] A [x; y] B (x A) & (y B)
By:
OrRight
THEN
OrRight
THEN
RWO
Thm*x:T, L:T List. (x L) [x] L
0
THEN
Try Obvious
Generated subgoals:
A
[x; y] 
[x; y] 
A) & (y 
x:T, L:T List. (x 
[x]