BINOP_TAC : tactic
A ?- f x1 y1 = f x2 y2 ================================ BINOP_TAC A ?- x1 = x2 A ?- y1 = y2
# g `f(2 * x + 1) + w * z = f(SUC(x + 1) * 2 - 1) + z * w`;;
# e BINOP_TAC;; val it : goalstack = 2 subgoals (2 total) `w * z = z * w` `f (2 * x + 1) = f (SUC (x + 1) * 2 - 1)`