Ramsey's theorem

[lowasser]

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.)