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`:
```lean
axiom classical.by_contradiction' {α : Sort*} : ¬ (α → false) → α
```
