This avoids `naive_solver` tearing whole goals apart, even if the goal
appears exactly as a hypothesis.

Get rid of using `Collection` and favor `set` everywhere. Also, prefer conversion
functions that are called `X_to_Y`.

The following sed script performs most of the renaming, with the exception of:

- `set`, which has been renamed into `propset`. I couldn't do this rename
  using `sed` since it's too context sensitive.
- There was a spurious rename of `Vec.of_list`, which I correctly manually.
- Updating some section names and comments.

```
sed '
s/SimpleCollection/SemiSet/g;
s/FinCollection/FinSet/g;
s/CollectionMonad/MonadSet/g;
s/Collection/Set\_/g;
s/collection\_simple/set\_semi\_set/g;
s/fin\_collection/fin\_set/g;
s/collection\_monad\_simple/monad\_set\_semi\_set/g;
s/collection\_equiv/set\_equiv/g;
s/\bbset/boolset/g;
s/mkBSet/BoolSet/g;
s/mkSet/PropSet/g;
s/set\_equivalence/set\_equiv\_equivalence/g;
s/collection\_subseteq/set\_subseteq/g;
s/collection\_disjoint/set\_disjoint/g;
s/collection\_fold/set\_fold/g;
s/collection\_map/set\_map/g;
s/collection\_size/set\_size/g;
s/collection\_filter/set\_filter/g;
s/collection\_guard/set\_guard/g;
s/collection\_choose/set\_choose/g;
s/collection\_ind/set\_ind/g;
s/collection\_wf/set\_wf/g;
s/map\_to\_collection/map\_to\_set/g;
s/map\_of\_collection/set\_to\_map/g;
s/map\_of\_list/list\_to\_map/g;
s/map\_of\_to_list/list\_to\_map\_to\_list/g;
s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
s/\bof\_list/list\_to\_set/g;
s/\bof\_option/option\_to\_set/g;
s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
s/seq\_set/set\_seq/g;
s/collections/sets/g;
s/collection/set/g;
' -i $(find -name "*.v")
```

This followed from discussions in https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/134

This is similar to `f_equal/=`.

As suggested by Pierre-Marie Pédrot in the Coq-club thread:

  [Coq-Club] Very slow failing apply

To work arround some performance issues in Iris.

It is sometimes not desirable to do so.

It no longer requires the functions on both sides of the relation
to be syntactically the same.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

case H; clear H would fail when H is dependent whereas destruct H
would succeed on that, but just not clear it.

The case tactic is faster than destruct.

Example:

Goal
  ¬False → ¬False → ¬False → ¬False → ¬False → ¬False → ¬False →
  False.
Proof.
  intros. done. (* takes very long *)

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

In particular, make sure we always try eassumption before reflexivity.

This has bothered me repeatedly in proofs, now I finally got around to fix it at the source

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

This is very experimental. It should now deal better with stuff like:

  match x with .. end = match y with .. end

In case there is a hypothesis H : R x y, it will try to destruct it.