CN: Simplify arguments to provable(withUnknown)

[dc-mak]

          I'm also a bit confused about all of the arguments to `provable`. I have a `Global.t` and a list of constraints that I want to check the consistency of. Christopher previously recommended adding all of the constraints to the solver as assumptions; should I still do that, or just `and` them together and make them the last argument? Would I leave the assumptions argument empty then? For `simp_ctxt`, can I follow the logic of `make_simp_ctxt` in typing.ml?

Originally posted by @cassiatorczon in #829 (comment)