Proofs written with the #Coq equations plugins are really interesting, because you end up using `rewrite` all the time.