||nil|| > 0 
hd(rev(nil)) = nil[(||nil||-1)] 
T4. v: T*
5. ||v|| > 0
hd(rev(v)) = v[(||v||-1)] ||u.v|| > 0 hd(rev(u.v)) = (u.v)[(||u.v||-1)] hd(rev(l)) = l[(||l||-1)]| 1 | ||nil|| > 0 hd(rev(nil)) = nil[(||nil||-1)] T |
| 2 | 3. u: T 4. v: T* 5. ||v|| > 0 hd(rev(v)) = v[(||v||-1)] ||u.v|| > 0 hd(rev(u.v)) = (u.v)[(||u.v||-1)] |
About:
 |  |  |  |  |  |  |  |