EQT_ELIM : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Eliminates equality with
T
.
DESCRIPTION
A |- tm = T ------------- EQT_ELIM A |- tm
FAILURE
Fails if the argument theorem is not of the form
A |- tm = T
.
SEEALSO
EQT_INTRO
,
EQF_ELIM
,
EQF_INTRO
HOL
Kananaskis-14