SUBST_ALL_TAC : thm -> tactic
{A1,...,An} ?- t ================================= SUBST_ALL_TAC (A |- u = v) {A1[v/u],...,An[v/u]} ?- t[v/u]
# g `!p x y. 1 = x /\ p(x - 1) ==> p(x EXP 2 - x)`;;
# e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`1 = x`] 1 [`p (x - 1)`] `p (x EXP 2 - x)`
# e(FIRST_X_ASSUM(SUBST_ALL_TAC o SYM));; val it : goalstack = 1 subgoal (1 total) 0 [`p (1 - 1)`] `p (1 EXP 2 - 1)`
# e(POP_ASSUM MP_TAC THEN CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[]);;