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_PFORALL universally 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_PFORALL ["x1";...;"xn"]
A |- (!x1...xn. t1) = (!x1...xn. t2)