Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
EQT_ELIM : thm -> thm
SYNOPSIS
Eliminates equality with T.
DESCRIPTION
A |- tm <=> T
--------------- EQT_ELIM
A |- tm
FAILURE CONDITIONS
Fails if the argument theorem is not of the form A |- tm <=> T.
EXAMPLE
# REFL `T`;;
val it : thm = |- T <=> T
# EQT_ELIM it;;
val it : thm = |- T