I was wondering how to translate
"\forall s in S. t(s)" into a let expression where t :: nat * nat.
let ?p = "ALL s. s : S --> t s < 0" isn't right since it has the type bool
=> bool, right? I'd want ?p to have the type nat, right?