And also rename the corresponding proof mode tactics.

This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.

rename program_logic.{ownership -> wsat}. It really is about world satisfaction and invariants more than about ownership.

Initial proof by Jan-Oliver Kaiser, adapted by Robbert Krebbers.

This allows us to factor out properties about connectives that
commute with the big operators.

Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.

As proposed by JH Jourdan in issue 34.

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.