\DOC VAR_EQ_TAC

\TYPE {VAR_EQ_TAC : tactic}

\SYNOPSIS
Simplifies a goal using any assumption of
the form {v = t} or {t = v}, where {v} is a variable

\KEYWORDS
simplification, rewriting, tactic.

\DESCRIBE
{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.

\FAILURE
{VAR_EQ_TAC} fails if there are no such assumptions

\SEEALSO
bossLib.FULL_SIMP_TAC, bossLib.ASM_SIMP_TAC, Rewrite.ASM_REWRITE_TAC

\ENDDOC