rule mul_annhil_rev(e, X) => mul(e, X)
rule left_inv_rev(e, X) => mul(inv(X), X)
proof
    e
    *mul_annhil_rev(e, b)
    mul(e, b)
    mul(*left_inv_rev(e, b), b)
    mul(mul(inv(b), b), b)
qed