GSUBST_TAC is the basic substitution tactic by means of which other
tactics such as SUBST_OCCS_TAC and SUBST_TAC are defined. Given a
list [(v1,w1),...,(vk,wk)] of pairs of terms and a term w, a
substitution function replaces occurrences of wj in w with vj
according to a specific substitution criterion. Such a criterion may
be, for example, to substitute all the occurrences or only some
selected ones of each wj in w.
Given a substitution function sfn,
GSUBST_TAC sfn [A1|-t1=u1,...,An|-tn=un] (A,t)
replaces occurrences of ti in t with ui according to sfn.
The assumptions of the theorems used to substitute with are not added
to the assumptions A of the goal, while they are recorded in the proof. If
any Ai is not a subset of A (up to alpha-conversion), then
GSUBST_TAC sfn [A1|-t1=u1,...,An|-tn=un] results in an invalid tactic.
A ?- t
============================= GSUBST_TAC sfn [A1|-t1=u1,...,An|-tn=un]
A ?- t[u1,...,un/t1,...,tn]
GSUBST_TAC automatically renames bound variables to prevent free variables in
ui becoming bound after substitution.