f_equiv optimizations

See merge request iris/stdpp!325

f_equiv: slightly better support for function relations

See merge request iris/stdpp!326

add size_set_seq

See merge request iris/stdpp!323

add size_difference

See merge request iris/stdpp!324

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

See merge request !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 !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 !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