The Infinite Pigeonhole Principle says: if you distribute infinitely many items among finitely many bins, at least one bin gets infinitely many items. In classical mathematics, this is trivial — a finite pigeonhole argument iterated. In constructive mathematics, where you must explicitly produce the infinite bin and its contents, the proof is hard. You need to find which bin overflows, and you can't search infinitely many items in finite time.
Pédrot & Tabareau (arXiv:2603.04006) give a constructive proof using two tools that usually don't combine: corecursion (producing infinite output lazily, one piece at a time) and callcc (capturing the current continuation — a control operator from programming that lets you “save your place” and return to it later).
Corecursion handles the infinite output. The proof produces a stream of items all belonging to one bin, generating each element on demand without ever completing. callcc handles the search. When the algorithm tentatively assigns items to bins, callcc captures the current state. If a bin fills up, the continuation returns control to the point where the winning bin was identified.
The termination guarantee comes from coiteration alone — no external argument about decreasing measures or well-founded orders. The proof terminates structurally, meaning the type system itself guarantees progress. This is the technical achievement: marrying a classical reasoning principle (callcc, which corresponds to classical logic) with a structural termination guarantee (corecursion), without requiring the general recursion that usually accompanies classical control operators.
The same technique implements the Axiom of Countable Choice — another principle that's trivial classically but requires explicit construction in the constructive setting. The general pattern: classical reasoning provides the search, corecursion provides the infinite witness, and the type system provides the termination.