avoid deprecated Proof <term>.

I didn't even know this was a thing, and it seems the Coq devs consider it deprecated and won't fix the issues it has (it doesn't properly work in ProofGeneral).

I have no idea why we have used this, but the alternative seems fine. So merging.

mentioned in commit e04271e2

merged