Note that the proof which derives a contradiction from the assumption that there is a largest prime is not constructive, since it does not explicitly give a way to compute an even larger prime. To turn this proof into a constructive one we have to show explicitly how to construct the larger prime. (Since proposition (\ref{prop1}) above is a \(\Pi^0_2\)-formula we can for example use Friedman’s A-translation to turn such a proof in classical arithmetic into a proof in intuitionistic arithmetic and thus into a proof in intuitionistic type theory.)