Skip to content

Add Pigeon Hole principle.

Robbert Krebbers requested to merge robbert/pigeon_hole into master

I was surprised that we do not have the Pigeon hole principle. It's a trivial consequence of results we already have on Finite types and cardinalities.

Merge request reports