SUBST1_TAC : thm_tactic
A ?- t ============= SUBST1_TAC (A' |- u = v) A ?- t[v/u]
# g `!p x y. 1 = x /\ p(1) ==> p(x)`;;
# e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`1 = x`] 1 [`p 1`] `p x`
# e(FIRST_X_ASSUM(SUBST1_TAC o SYM));; val it : goalstack = 1 subgoal (1 total) 0 [`p 1`] `p 1`