add mk_evar tactic (to replace Coq's strange evar tactic) and use it

See merge request !289

Make `done` work on `is_Some`.

See merge request !293

Fix priority of `Permutation_app'`.

Closes #114

See merge request !291

add lookup_union_l

See merge request !292

This is a workaround for https://github.com/coq/coq/issues/14571

This fixes #114.

Update changelog for filter extensionality lemmas

See merge request !290

Make sum_inhabited_r not a copy of sum_inhabited_l

See merge request !288

This existed at least as far back as
361308c7, 8 years ago.

rename insert_delete → insert_delete_insert; add new insert_delete matching delete_insert

See merge request !287

Add a few set and map related lemmas

See merge request !284

Fix potential stack overflow related to `Pretty N`.

See merge request !286

add {fst,snd}_map_zip

See merge request !285

Rewrite cross split lemmas so they can more easily be used for forward reasoning.

See merge request !283

Various setoids lemmas for maps, lists, and option

See merge request !281

Add lemmas `map_intersection_filter` and `map_difference_filter`.

See merge request !282