Revert "Merge branch 'robbert/sprop' into 'master'"

See merge request iris/stdpp!322

This reverts merge request !309

Use `SProp` to obtain better definitional equality for  `pmap`, `gmap`, `gset`, `Qp`, and `coPset`

Closes #85

See merge request iris/stdpp!309

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 iris/stdpp!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