rule right_id(mul(X, e)) => X
rule left_id(mul(e, X)) => X
rule assoc_left(mul(mul(A, B), C)) => mul(A, mul(B, C))
rule left_inv(mul(inv(X), X)) => e

proof
    mul(a, e)
    *right_id(mul(a, e))
    a
qed