RES_FORALL_SWAP_CONV : conv
STRUCTURE
res_quanLib
SYNOPSIS
Changes the order of two restricted universal quantifications.
DESCRIPTION
When applied to a term of the form
!x::P. !y::Q. R
, the conversion
RES_FORALL_SWAP_CONV
returns the theorem:
|- (!x::P. !y::Q. R) = !y::Q. !x::P. R
providing that
x
does not occur free in
Q
and
y
does not occur free in
P
.
FAILURE
Fails if applied to a term not of the correct form.
SEEALSO
RES_FORALL_CONV
HOL
Kananaskis-13