list_mk_res_exists : ((term # term) list # term) -> term)
STRUCTURE
res_quanLib
SYNOPSIS
Iteratively constructs a restricted existential quantification.
DESCRIPTION
   list_mk_res_exists([("x1","P1");...;("xn","Pn")],"t")
returns "?x1::P1. ... ?xn::Pn. t".
FAILURE
Fails with list_mk_res_exists if the first terms xi in the pairs are not a variable or if the second terms Pi in the pairs and t are not of type ":bool" if the list is non-empty. If the list is empty the type of t can be anything.
SEEALSO
strip_res_exists, mk_res_exists
HOL  Trindemossen-1