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)