At:
singelton append equals lemma
1
2
1
1.
T: Type
2.
a: T
3.
S: T List
4.
b: T
5.
u: T
6.
v: T List
7.
[a] = [u; 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:
None
About:
