I was reading https://github.com/coq/coq/wiki/CoqAndAxioms, it says that strong excluded middle axiom is derivable from indefinite description and the excluded middle.

I'm trying but for now I'm unsuccessful. Any hints?

Use the fact that `A + ~A`

is isomorphic to `{b : bool & if b then A else ~A}`

, and then use choice to go between Prop and Type.

you can also use that `ex (fun _ : A + B => True)`

is equivalent to `A \/ B`

Thank you both.

Lessness has marked this topic as resolved.

Last updated: Oct 01 2023 at 19:01 UTC