VAR_EQ_TAC
BasicProvers.VAR_EQ_TAC : tactic
Simplifies a goal using any assumption of the form v = t or t = v,
where v is a variable
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
See also
bossLib.FULL_SIMP_TAC,
bossLib.ASM_SIMP_TAC,
Rewrite.ASM_REWRITE_TAC