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) → α
```

src/logic/basic.lean

@@ -1144,6 +1144,14 @@ hpq _ $ some_spec _
 noncomputable def subtype_of_exists {α : Type*} {P : α → Prop} (h : ∃ x, P x) : {x // P x} :=
 ⟨classical.some h, classical.some_spec h⟩
 
+/-- A version of `by_contradiction` that uses types instead of propositions. -/
+protected noncomputable def by_contradiction' {α : Sort*} (H : ¬ (α → false)) : α :=
+classical.choice $ peirce _ false $ λ h, (H $ λ a, h ⟨a⟩).elim
+
+/-- `classical.by_contradiction'` is equivalent to lean's axiom `classical.choice`. -/
+def choice_of_by_contradiction' {α : Sort*} (contra : ¬ (α → false) → α) : nonempty α → α :=
+λ H, contra H.elim
+
 end classical
 
 /-- This function has the same type as `exists.rec_on`, and can be used to case on an equality,