This fixes issue #72.

It now first turns hypotheses `X ∪ Y ⊆ Z` into `X ⊆ Z` and `Y ⊆ Z`.

Add IntoPure instances for ∗, ∧, and ∨.

See merge request !49

Add a contributor's guide

See merge request !47

When using [iAssert ... with ">[]"], we should not use [tac_assert_persistent], and eliminate the modality instead.

This patch is still not ideal, because some modalities (e.g., later) preserve persistence.

For example, when having `"H" : ∀ x : Z, P x`, using
`iSpecialize ("H" $! (0:nat))` now works. We do this by first
resolving the `IntoForall` type class, and then instantiating
the quantifier.

Instead of doing all the instantiations by invoking a single type
class search, it now performs the instantiations by invoking
individual type class searches. This a.) gives better error messages
and b.) works when `xj` depends on `xi`.

In the following ways:
- When having `P → Q` it will now also work when the spatial context
  is non-empty.
- When having `∀ x : A, Q` it will now do an `iIntros (_)`.

Make it possible to apply the observational view shift lemmas.

See merge request !40