Axioms
Axioms are propositions postulated without proof. There are seven standard axioms, three of which have mathematical content.[…]Three of the remaining axioms concern performance optimizations whose soundness rests on the compiler beyond the kernel. The final one is used by sorry. These three are the quotient axiom, propositional extensionality, and the axiom of choice. The first two are similar in that they postulate equality assuming equivalence.