add size_set_seq

See merge request !323

add size_difference

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

add map_size_disj_union

See merge request !321

bring back some empty_inv lemmas for rewriting

See merge request !317