Use high cost for `Decision` instances for `True` and `False`.

Closes #165

See merge request !434

add size_list_to_map

See merge request !431

option.v: Add option_guard_decide and option_guard_bool_decide

See merge request !433

Motivated by https://mattermost.mpi-sws.org/iris/pl/cz6f4bxwsir78jkunk7nt3bawo.

proof by Robbert Krebbers

add map_zip_with_empty lemmas

See merge request !430

Tweak `f_equiv` to use `reflexivity` in a way similar to `f_equal`.

See merge request !428

make solve_ndisj work on goals of the form 'X1 ∪ X2 ## Y'

See merge request !427

Use `notypeclasses refine` for `TCIf` and `TCNoBackTrack`.

See merge request !426

Add tactic `tc_solve`.

See merge request !425

Fix unfolding logic of bv_simplify

See merge request !411

Use `eauto` as default for `set_solver`.

See merge request !420

add gset_to_gmap_to_list

See merge request !422

Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.

See merge request !419