Misc improvements to `head` and `tail` functions for lists

• Define head as notation that prints (Coq defines it as parsing only).
• Declare tail as simpl nomatch.
• Add lemmas about head and tail.