bring back some empty_inv lemmas for rewriting

See merge request !317

relations lemmas

See merge request !316

add some lookup_{union,difference} lemmas

See merge request !315

add get_head tactic and use it in solve_proper_unfold

See merge request !311

add insert_map_seq_0

See merge request !314

add lookup_take_Some

See merge request !313

add binder_list

See merge request !312

Mark gset methods as simpl never to stop `cbn` from unfolding them

See merge request !298

Add more lemmas for FinMaps (for union, filter, difference)

See merge request !245

Generalize `map_filter_insert` so that it covers both the True and False case.

See merge request !310

Use `_True` and `_False` for the specific cases.

Weaken premise of `map_filter_delete_not` and make it consistent with `map_filter_insert_not'`.

Clean up `empty{',_inv,_iff}` lemmas.

See merge request !307