Before this commit, given "HP" : P and "H" : P -★ Q with Q persistent, one
could write:

  iSpecialize ("H" with "#HP")

to eliminate the wand in "H" while keeping the resource "HP". The lemma:

  own_valid : own γ x ⊢ ✓ x

was the prototypical example where this pattern (using the #) was used.

However, the pattern was too limited. For example, given "H" : P₁ -★ P₂ -★ Q",
one could not write iSpecialize ("H" with "#HP₁") because P₂ -★ Q is not
persistent, even when Q is.

So, instead, this commit introduces the following tactic:

  iSpecialize pm_trm as #

which allows one to eliminate implications and wands while being able to use
all hypotheses to prove the premises, as well as being able to use all
hypotheses to prove the resulting goal.

In the case of iDestruct, we now check whether all branches of the introduction
pattern start with an `#` (moving the hypothesis to the persistent context) or
`%` (moving the hypothesis to the pure Coq context). If this is the case, we
allow one to use all hypotheses for proving the premises, as well as for proving
the resulting goal.

Define disjointness of namespaces in terms of masks.\n\nThe proofs are made simpler and some lemmas get more general.

I had to perform some renaming to avoid name clashes.

This way we ensure that Coq gives an error message when one accidentially
writes "N ⊆ E" instead of "nclose N ⊆ E". Before, it used the ⊆ instance of
lists.

This avoids Coq distinguishing iProp and uPred (iResUR _) when it
should not.

(which are useful in Amin's logical relations development).

This also removes the double use of the name 'wp_fork' in both
program_logic/weakestpre and heap_lang/lifting.

Following the time anology of later, the step-index 0 corresponds does
not correspond to 'now', but rather to the end of time (i.e. 'last').

Make names more consistent with the rest of the development, make
definitions type classes opaque so that the proofmode does not unfold
then, declare timeless, persistent and proper instances.

This implements issue #3.

Since [inG] ranges over [cmraT]s, using an [ucmraT]s results in
[ucmra_cmraR] coercions that slow down type checking.

This commit improves the compilation time of thread_local.v by 40%.

By using the global ghost maps instead of our own ones.

It is not non-expansive, so not a function we should use.

This generalization is surprisingly easy in Iris 3.0, so I could not
resist not doing it :).

This makes stuff more uniform and also removes the need for the [inGFs]
type class. Instead, there is now a type class [subG Σ1 Σ2] which expresses
that a list of functors [Σ1] is contained in [Σ2].