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