Ramsey's theorem #1845
Description
The main missing ingredient is the strong pigeonhole principle, though there's a lot of refactoring and cleanup work I find myself wanting to do in univalent-combinatorics first. (#1836 in particular is attempting to work in that direction.)