Annotate telescope notations to support literal telescope arguments.

See merge request iris/stdpp!375

Add Pigeon Hole principle.

See merge request !373

Add induction principle for `tele_arg`.

See merge request iris/stdpp!374

Define [tele_arg] as a fixpoint

See merge request !368

Clarify relationship between `gset_to_gmap` and `set_to_map`.

See merge request !371

Add lemmas list_to_set_disj_elem_of_list and gmultiset_difference_disj_union_{l,r}

See merge request !369

Avoid universe bumps of `gset`/`mapset` (fixes #134)

Closes #134

See merge request !370

Workaround to avoid `injection` from unfolding equalities on `dom`

See merge request iris/stdpp!367

Add set_unfold_list_bind (+ test)

See merge request iris/stdpp!366

`set_unfold_bind` for sets already exists; this brings the list variant on par.