Application of LAST_FORALL_CONV v to the term
``!x1 .. xn x. body`` will apply c to the term ``!x. body``.
If the result of this application is the theorem |- (!x. body) = t, then
the result of the whole will be
|- (?x1 .. xn x. body) = (?x1 .. xn. t)