Refactor and improve documentation of feed and efeed tactics

See merge request iris/stdpp!403

Refactor feed and add the feed generalize, efeed generalize, efeed inversion, and efeed destruct tactics

Rename plus/minus → add/sub and put number lemmas in modules to be consistent with Coq stdlib

See merge request iris/stdpp!404

This is similar to the trick we use for `bi` and makes it possible to import
`Nat` and obtain all lemmas---i.e., those from Coq's stdlib + those from std++.

Thanks to @Blaisorblade for the suggestion.

Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current convention for numbers.

add some very basic f_equiv tests

See merge request iris/stdpp!409

[list] restricted version of list_fmap_equiv_ext

See merge request iris/stdpp!384

Generalize Propers for lists / Add some missing Params

See merge request iris/stdpp!407

Create stdpp-unstable package and add bitblast library

See merge request iris/stdpp!402

Some `filter` lemmas make use of `map_Forall`, so put `map_Forall` before `filter.

Introduce `set_bind` and associated lemmas + set_bind theory: revise setoid rewriting

See merge request iris/stdpp!406

- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances can be proven before `set_bind_ext` via `set_solver`.
- `set_bind_ext` is then provable by set_solver directly.