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_INTRO : thm -> thm
SYNOPSIS
Introduces equality with T.
DESCRIPTION
A |- tm
--------------- EQF_INTRO
A |- tm <=> T
FAILURE CONDITIONS
Never fails.
EXAMPLE
# EQT_INTRO (REFL `2`);;
val it : thm = |- 2 = 2 <=> T