VAR_EQ_TAC : tactic
STRUCTURE
SYNOPSIS
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.

FAILURE
VAR_EQ_TAC fails if there are no such assumptions
SEEALSO
HOL  Kananaskis-14