At:
equal appends eq12
1.
T: Type
2.
x1: T List
3.
z: T List
4.
x2: T List
5.
x3: T List
6.
||x1|| = ||z||
7.
(x1 @ x2) = (z @ x3)
8.
u: T
9.
v: T List
10.
z = (x1 @ [u / v])
11.
x2 = ([u / v] @ x3)
x1 = z & x2 = x3
By:
MoveToConcl 6
THEN
SubstFor z 0
THEN
RWO
Thm*as,bs:T List. ||as @ bs|| = ||as||+||bs||
0
Generated subgoals:
x1 = z & x2 = x3
as,bs:T List. ||as @ bs|| = ||as||+||bs||