axiom of choose: 面白い

[shnarazk]

4.2, p.61

variable {α β : Type*} [Inhabited α]

#check (default : α)

variable (P : α → Prop) (h : ∃ x, P x)

#check Classical.choose h

example : P (Classical.choose h) := Classical.choose_spec h