Fix a couple of proofs broken by change to MAX_SET definition.