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.