FIND_ASSUM : thm_tactic -> term -> tactic
# g `0 = x /\ y = 0 ==> f(x + f(y)) = f(f(f(x) * x * y))`;;
# e STRIP_TAC;; val it : goalstack = 1 subgoal (1 total) 0 [`0 = x`] 1 [`y = 0`] `f (x + f y) = f (f (f x * x * y))`
# e(FIND_ASSUM SUBST1_TAC `y = 0` THEN FIND_ASSUM (SUBST1_TAC o SYM) `0 = x`);; val it : goalstack = 1 subgoal (1 total) 0 [`0 = x`] 1 [`y = 0`] `f (0 + f 0) = f (f (f 0 * 0 * 0))`
# e(REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES]);; val it : goalstack = No subgoals
# e(REWRITE_TAC[ASSUME `y = 0`; SYM(ASSUME `0 = x`); ADD_CLAUSES; MULT_CLAUSES]);;