Theorems that require decidability hypotheses are in the namespace "decidable". Classical versions are in the namespace "classical".

Note: in the presence of automation, this whole file may be unnecessary. On the other hand, maybe it is useful for writing automation.

pempty

pempty is the universe-polymorphic analogue of empty.

forall_iff_forall_surj

A predicate holds everywhere on the image of a surjective functions iff it holds everywhere.

classical.subtype_of_exists

A version of classical.indefinite_description which is definitionally equal to a pair