Abstract Proof Checking: An Example Motivated by an Incompleteness Theorem