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(mul(a, e), mul(e, a))
    mul(*right_id(mul(a, e)), mul(e, a))
    mul(a, mul(e, a))
    mul(a, *left_id(mul(e, a)))
    mul(a, a)
qed