LIST_MK_EXISTS : (term list -> thm -> thm)

- STRUCTURE
- 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 xi 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
- 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.
- SEEALSO

HOL Kananaskis-14