Normalize focused goal output

See merge request iris/stdpp!330

Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line,
since this is the new output in Coq 8.15+.

std++ does not currently produce this output, since no test calls `Show`
with shelved goals, but this future-proofs the test normalization.

fin_sets: add missing Params instance for `set_map`

See merge request iris/stdpp!328

Noticed from VERY slow rewrites.

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 !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.