I don't understand. The relevant step in the argument, as far as I understand it, requires an inference from "there exists a proof in n steps that cooperate is better" to "the agent cooperates". It seems to me that "enumerating all shorter proofs" would requiring knowing the precise proof (or at least its length), not just the statement "there exists such a proof". But I'm probably not following what, exactly, you have in mind; could you expand on your argument?

[I should say I was wrong to say "it ... cannot prove that" above -- all I can say is that one particular technique for showing that it can prove it doesn't go through.]