refactor: simplify excluded middle proof

[james-smith-a8e6]

The current Classical.em proof isn't that easy to follow. Since Lean has quotients, we can take a two-element type like Bool, and quotient it by x = y ∨ P. Then, the surjection Bool → A splits and we use the fact that Bool has decidable equality to decide P.

Based on proof at https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theorem.

[leodemoura]

Marking as low priority. Lean has proof irrelevance. Thus, this commit does not benefit users.