LAST_FORALL_CONV

Conv.LAST_FORALL_CONV : conv -> conv

Applies a conversion to the last universal quantifier (and its body) in a chain.

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)

Failure

Fails if the term is not universally quantified, or if the conversion c fails when it is applied.

See also

Conv.BINDER_CONV, Conv.LAST_EXISTS_CONV, Conv.STRIP_QUANT_CONV