list_mk_exists : term list * term -> term

SYNOPSIS

Multiply existentially quantifies both sides of an equation using the given variables.

DESCRIPTION

When applied to a list of terms [x1;...;xn], where the ti are all variables, and a theorem A |- t1 = t2, the inference rule LIST_MK_EXISTS existentially quantifies both sides of the equation using the variables given, none of which should be free in the assumption list.

              A |- t1 <=> t2
   ----------------------------------------  LIST_MK_EXISTS [`x1`;...;`xn`]
    A |- (?x1...xn. t1) <=> (?x1...xn. t2)

FAILURE CONDITIONS

Fails if any term in the list is not a variable or is free in the assumption list, or if the theorem is not equational.

SEE ALSO

MK_EXISTS.