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, inv(b)), b)
    *assoc_left(mul(mul(a, inv(b)), b))
    mul(a, mul(inv(b), b))
    mul(a, *left_inv(mul(inv(b), b)))
    mul(a, e)
    *right_id(mul(a, e))
    a
qed