At:
append one one12
1.
T: Type
2.
x: T List
3.
z: T List
4.
y: T List
5.
w: T List
6.
||x|| = ||z|| ||y|| = ||w||
7.
(x @ y) = (z @ w)
8.
u: T
9.
v: T List
10.
x = (z @ [u / v]) & w = ([u / v] @ y) z = (x @ [u / v]) & y = ([u / v] @ w)
[u / v] = nil
By:
SplitOrHyps
THEN
AllHyps
(h.
(ApFunToHypEquands `l' ||l|| h)
THEN
(RWO
Thm*as,bs:T List. ||as @ bs|| = ||as||+||bs||
-1))
Generated subgoals:
||y|| = ||w|| 
[u / v] = nil
h.
(ApFunToHypEquands `l' ||l|| 
as,bs:T List. ||as @ bs|| = ||as||+||bs||