Control whether provider decls accept postulates

Extends the provider syntax to accept an optional "what" parameter,
which controls if it can be satisfied with just proof terms, just
postulates, or either.