I define the following axiom.
(First, I want to prove it, and make it Theorem. However, I can not find how to start.)
Axiom functions_eq_or_not : forall f g : (Q -> bool), (forall q : Q, f q = g q) \/ (exists q : Q, f q <> g q).
Can I prove it (without using excluded middle) and make it Theorem?