This should ensure that `coqchk` no longer reports axioms.

1. Improve naming
2. Make `wf_` proofs of `gmap` and `pmap` opaque
3. Avoid `bind` and `fmap` combinators for `SProp`
4. Drop `simpl` tests

Items 2-3 are crucial for performance, otherwise each operation checks if the map
is still well-formed, which destroys log(n) complexity of map operations.

Why 3 is needed is subtle: The `bind` and `fmap` lemmas for `SProp` contain Booleans
as implicit arguments, which are eagerly evaluated by `vm_compute`.

As a result of 2-3, `simpl` will not normalize proofs to `stt`, and `simpl` tests
do not give a desirable result.

add lemma list_in_dec

See merge request iris/stdpp!319

treat Forall2 constructors like we treat Forall constructors

See merge request !318

relate size of map to size of its domain

See merge request !320

add map_size_disj_union

See merge request !321

bring back some empty_inv lemmas for rewriting

See merge request !317

relations lemmas

See merge request !316

add some lookup_{union,difference} lemmas

See merge request !315

add get_head tactic and use it in solve_proper_unfold

See merge request !311

add insert_map_seq_0

See merge request iris/stdpp!314

add lookup_take_Some

See merge request !313