Simplifies a goal using any assumption of
the form v = t or t = v, where v is a variable
DESCRIPTION
VAR_EQ_TAC simplifies the goal, including its assumptions,
using one assumption of
the form v = t or t = v, where v is a variable
which is not contained in t.
In both cases, v is replaced throughout by t,
and the relevant assumption is deleted.