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