[remexre]

We had a joke that our PL course is a maturity test, because Coq and Hoare triples come up in the same lecture...