Further issues with in-Coq computation for pmap and gmap

These issues are discussed on Mattermost starting at https://mattermost.mpi-sws.org/iris/pl/o9tme6imrfdtf8chhwi6fr1kor. Basically, reducing gmaps will also reduce their well-formedness checks; I expect continuing the work in !106 (merged) and sealing well-formedness predicates would avoid the issue.

Of most interest are these comments:

Let me point out that computing gmap_wf_aux takes time linear in the sum of key sizes, and that plausibly explains the performance numbers that I saw back then, and the problem Greg mentions with large keys. Meanwhile, Pmap_wf has a smaller variant of the same problem (its cost does not depend on key sizes).

and Robbert's idea for Pmap:

Also, at some point I looked into a more intrinsic representation of finite maps that ensures the well-formedness condition without a Sigma-type. I have never finished that, but if someone wants to help working on this, feel free to get in touch.

The code is in https://mattermost.mpi-sws.org/iris/pl/6mkua571y7g35cqndt455y74rc; I expect some sealing would still be needed.