At:
singelton append equals lemma122
1.
T: Type
2.
a: T
3.
S: T List
4.
b: T
5.
u: T
6.
v: T List
7.
u1: T
8.
v1: T List
9.
[a] = u.(v1 @ (b.S)) a = b
10.
[a] = [u; u1/ v1 @ (b.S)]
a = b
By:
ApFunToHypEquands `L' (Case of L; nil 0 ; h.t Case of t; nil 1 ; h.t 2) -1
THEN
Reduce -1
Generated subgoals:
a = b
a = b
0 ; h.t 
-1
