Diaconescu's theorem: excluded middle from choice, Function extensionality and propositional extensionality.
All propositions are Decidable.
the Hilbert epsilon Function
the axiom of choice
by_cases (h :)? p splits the main goal into two cases, assuming h : p in the first branch, and h : ¬ p in the second branch.
by_cases (h :)? p
h : p
h : ¬ p