Fix a couple of proofs broken at a9c9add.