Proving uniqueness of group identity element

Question

Start, as in the Mathematica 11.3 documentation, with:

   groupTheory = {ForAll[{a, b, c}, g[a, g[b, c]] == g[g[a, b], c]], 
                  ForAll[a, g[a, e] == a], ForAll[a, g[a, inv[a]] == e]}

The result I want Mathematica to prove is the uniqueness of the identity e:

   uniqueIdentityThm = ForAll[f, Implies[ForAll[x, g[x, f] == x], f == e]]

If I try...

   FindEquationalProof[uniqueIdentityThm, groupTheory]

... then I get a surprising error message:

... FindEquationalProof: Invalid specification of propositions ....and axioms..

Do I have a syntax error I'm not seeing?

Or is the issue simply the presence of Implies?

Note that the general form of what I'm trying to do is OK, for example:

   inverseIsInvolution = ForAll[x, inv[inv[x]] == x
   FindEquationalProof[inverseIsInvolution, groupTheory]

This does yield a ProofObject, which can be examined, e.g., by evaluating the preceding result with argument "ProofNotebook".

Answer 1

Let us consider the axioms for a group:

groupTheory={ForAll[{a,b,c},g[a,g[b,c]]==g[g[a,b],c]],
  ForAll[a,g[a,e]==a],
  ForAll[a,g[a,inv[a]]==e]};

As shown in the question, Murray's command for proving that the right identity is unique:

FindEquationalProof[Implies[ForAll[a, g[a, f]==a], e==f], groupTheory ]

fails with a message that there is an invalid specification of propositions and axioms. This suggests (I am not sure at all) that the first argument of Implies is considered as an axiom, that should be placed in the second argument of FindEquationalProof. Anyway, the unicity can be shown with Mathematica in the following way:

FindEquationalProof[e==f, Append[groupTheory, ForAll[a, g[a, f]==a] ]]

(* ProofObject[Logic: EquationalLogic   Steps: 10 ...] *)

And for sake of completeness, Mathematica can show that any right identity is also a left identity:

FindEquationalProof[ForAll[a, g[e, a]==a], groupTheory ]

(* ProofObject[Logic: EquationalLogic   Steps: 11 ...] *)