Postulate providers

Now, type providers don't need to return a proof - they can postulate
new axioms. The intention is to connect this both to QuickCheck and to
external proof oracles, such as SMT solvers.
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.
Merge pull request #937 from david-christiansen/postulate-providers

Postulate providers