Hi all,Is there a way to have a quantification over a finite set of names; something like
ALL (finite name B) P.P is another type. I am confused about the syntax of the finite set in HOL.
In list would be something like: ALL (B :: name list) P. Thanks in advance for any help. -T