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