port to gen_proofmode

Unfortunately rewrite stopped working in a few cases, which I worked around because I did not know how to fix it.

Cc @robbertkrebbers