Improve notations and modal tactics
Add file to investigate automation in Coq
Start using fancy verbatim