useful notations

[DanGrayson]

Notation such as

Local Notation "[]" := nil (at level 0, format "[]").
Local Infix "::" := cons.

in Lists.v should be made non-local and put into a scope so when the file Lists is imported and the scope is opened, the importing file has access to the notation.

The level declaration should be moved to Foundations/Init.v.