----------------------------------------------------------------------
VAR_EQ_TAC                                              (BasicProvers)
----------------------------------------------------------------------
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.

----------------------------------------------------------------------