Make Waterproof work with bullets and braces

[jim-portegies]

One way of structuring proofs in Coq is to use bullets and braces. This behavior can be enforced by Set Default Goal Selector "!".

However, it seems that errors thrown by Coq about this are not presented to the end user, which is confusing.

Also it seems that in the presented code, indentation on the first line is stripped, which causes checkmarks to appear at wrong places.