||rev(v) @ [u]||
1 ||v||+1 > 0 
hd((rev(v) @ [u])) = u hd(rev(v)) = v[(||v||-1)] ||v||+1 > 0 hd((rev(v) @ [u])) = (u.v)[(||v||+1-1)]
a:T, as:T*, i:
. i
0 (a.as)[i] = a)
0| 1 | 7. ||v||+1 > 0 ||rev(v) @ [u]||1 |
| 2 | ||v||+1 > 0 hd((rev(v) @ [u])) = u |
About:
 |  |  |  |  |  |
 |  |  |  |  |