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
COMB_CONV : conv -> conv
SYNOPSIS
Applies a conversion to the two sides of an application.
DESCRIPTION
If c is a conversion such that c `f` returns |- f = f' and
c `x` returns |- x = x', then COMB_CONV c `f x` returns
|- f x = f' x'. That is, the conversion c is applied to the two
immediate subterms.
FAILURE CONDITIONS
Never fails when applied to the initial conversion. On application to the term,
it fails if conversion given as the argument does, or if the theorem returned
by it is inappropriate.