This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.

This follows iris!387
This closes issue #54.

The opposite was true before to this commit.

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.