functor (S : Set.S) ->
  functor (P : sig type p = S.elt val p : p predicate end) ->
    sig
      val exists : S.t Specification.predicate
      val for_all : S.t Specification.predicate
    end