Added a simplification function to simplify expressions using a given equality a = b + c, by replacing occurences of e.g. b + c by a, or a - b by c.
a = b + c
b + c
a
a - b
c