Commit 2021-08-31 09:04 c04e8a48
View on Github →feat(logic/basic): equivalence of by_contra and choice (#8912)
Based on an email suggestion from Freek Wiedijk: classical.choice is equivalent to the following Type-valued variation on by_contradiction:
axiom classical.by_contradiction' {α : Sort*} : ¬ (α → false) → α