Given a theorem A'|-u=v and a goal (A,t), the tactic
SUBST1_TAC (A'|-u=v) rewrites the term t into t[v/u], by substituting
v for each free occurrence of u in t:
The assumptions of the theorem used to substitute with are not added
to the assumptions of the goal but are recorded in the proof. If A' is not a
subset of the assumptions A of the goal (up to alpha-conversion), then
SUBST1_TAC (A'|-u=v) results in an invalid tactic.
A ?- t
============= SUBST1_TAC (A'|-u=v)
A ?- t[v/u]
SUBST1_TAC automatically renames bound variables to prevent free variables in
v becoming bound after substitution.