At: hd reverse 1 2 1 1 1
1. T: Type
2. l: T*
3. u: T
4. v: T*
5. ||v|| > 0 
hd(rev(v)) = v[(||v||-1)]
6. ||v|| = 0
7. ||v||+1 > 0
||rev(v) @ [u]||
1
By:
RWH
(LemmaC
Thm* 
as,bs:T*. ||as @ bs|| = ||as||+||bs||)
0
THEN
Reduce 0
Generated subgoals:None
About:
