When applied to a list of terms [p1;...;pn], where the pi are all
paired structures of variables, and a theorem A |- t1 = t2,
the inference rule LIST_MK_PEXISTS existentially quantifies both sides
of the equation using the pairs given, none of the variables in the pairs
should be free in the assumption list.
A |- t1 = t2
-------------------------------------- LIST_MK_PEXISTS ["x1";...;"xn"]
A |- (?x1...xn. t1) = (?x1...xn. t2)