Reduction from Diophantine equations to provability in IPC2 / System F.
This proof is now integrated into the Coq Library of Undecidability Proofs as theorem H10C_SAT ⪯ SysF_INH. This provides a constructive many-one reduction from the Halting problem to System F inhabitation as theorem HaltTM 1 ⪯ SysF_INH.