Proofs involving multiple arguments

I've been looking again at Oliver Charles' great authorization-via-ghosts-of-departed-proofs [blog post](https://ocharles.org.uk/blog/posts/2019-08-09-who-authorized-these-ghosts.html), and it kind of annoyed me that after quite a beautiful setup, he then has to manually do the `pricePolicy` work. Moreover, the API doesn't see the proof terms, which is sad. They would have been nice documentation...

It occurred to me we could have something like

``` haskell
-- in CanRead.hs . CanRead constructors not exported
data CanRead user project = CanRead

-- "Given" is a two param version of the one in `reflection`
instance (Given user User, Given projectId ProjectId)
=> Provable (CanRead user projectId) where
-- Note that if I need e.g. a DB connection, I can also just use *Given*
--- it'll pluck things out of the Context
prove :: IO (Maybe (CanRead user projectId))
prove = ...

-- API.hs
type API = AuthN "user" User
:> CaptureN "projectId" ProjectId
:> Proof ("user" `CanRead` "projectId")
:> Get '[JSON] Project

-- deduced handler type. But note users could *write* with type variables, as with normal GDP
handler :: Named "user" User -> Named "projectId" ProjectId -> CanRead "user" "projectId" -> Handler Project
handler = ...
```

So, I'm proposing servant could allow for the `Proof` construct, which can pick the right arguments from the API (mostly using the type-level string annotations that we have so far), use those to (a la [reflection](https://hackage.haskell.org/package/reflection-2.1.5/docs/Data-Reflection.html#v:give)) check that the proof is good, otherwise errorring out automatically (status codes etc tbd), in a way that is pretty much as water tight as GDP.

(Very briefly, the trick is to feed everything that might be need in a proof into the Context, then at each Proof type, pull out all the things and `give` them to `prove` at the `Proof` type. This can also be used to pass in the e.g. `Connection` I mentioned above.)

I've played around a bit, and think this should work. Should I submit a PR for it? There would be some changes to the constraints in HasServer instances, but they'll be met in the same conditions in practice, so that I think this is mostly backwards compatible. However, ideally (for reasons I can get into) it is safer if we verify that, for any endpoint, the set of type-level strings used (in Capture, QueryParam, etc) are unique, type-erroring if not. That, of course, would not be backwards compatible.

Named versions of combinators (one's that correspond to `Named` type) would be introduced. Actually, probably just one - everything else could be a type synonym.