Added some Coq examples.
Formatting and readaibility improvements.
Wrote out the `elem` example.
Wrote about some introductory examples on erasure.