Theorem AC_to_LEM : AxiomOfChoice -> LEM. Proof. intros AC P. set (f := setquotpr _ : bool -> setquotinset (eqrel_on_bool P)). assert (q := pr1 AC_impl2 AC _ _ f (issurjsetquotpr _)). apply (squash_to_prop q). { apply isapropdec, propproperty. } intro sec. induction sec as [g h]. apply (logeq_dec (eqrel_on_bool_iff P)). apply (retract_dec f g h isdeceqbool). Defined.