congruence transformation
After getting stuck on goals of the form f a1 b1 c1 = f a2 b2 c2
with a1 = a2, b1 = b2, c1 = c2
, I added a transformation to handle this.
This is equivalent to Coq's f_equal
tactic but only handles the case where the function symbols are the same.