Add lemma `map_singleton_subseteq_l` and `map_singleton_subseteq`.

See merge request iris/stdpp!308

Make singleton/`⊆` lemmas consistent with Iris's singleton/`≼`

See merge request iris/stdpp!306

Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l` and swap order to be consistent with Iris's `singleton_included_l`.

Add lemmas that say that `curry{3,4}?` and `uncurry{3,4}?` are inverses.

See merge request iris/stdpp!304

solve_ndisj: handle goals containing _ ∖ _ ∖ _

See merge request iris/stdpp!303

`Params` and `Proper` instances for `curry` and friends

See merge request iris/stdpp!302

solve_ndisj: solve more goals involving chains of differences

See merge request iris/stdpp!300

rename map_union_subseteq_l_alt → map_union_subseteq_l' (and likewise for _r)

See merge request iris/stdpp!301

Swap `curry` and `uncurry` to be consistent with Haskell and friends.

Closes #76

See merge request iris/stdpp!297

This also applies to `(un)curry{3,4}`, `gmap_(un)curry`, and `h(un)curry`.

This fixes issue #76.

The code includes a horrible hack that should removed once support for Coq versions prior
to 8.13 is dropped.

alternative implementation of mk_evar that keeps naive_solver working

Closes #115

See merge request iris/stdpp!299

handle more goals in solve_ndisj

See merge request iris/stdpp!294