rvs is (classically) equivalent to a kind of double negation

Proofs showing that rvs is equivalent to a kind of step-indexed double negation modality under classical axioms. For now, placed in algebra/double_negation.v until the new directory structure is finalized.

cc: @jung @robbertkrebbers 

See merge request !8

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.

Annoyingly, this requires one to prove the following in the model:

  (∀ x : A, ■ φ x) ⊢ ■ (∀ x : A, φ x)

Thanks to Ranald Clouston for suggesting the axiom:

  ▷ P ⊢ ▷ False ∨ (▷ False → P)

This axiom is used to prove timeless of implication, wand and forall.

Timelessness of the pure and ownM connectives is still proven in the model, but
we first state the property in a way that it does not involved derived notions
(like the except_last modality).

It is unused, and ownM_empty is stronger.

For that we need a slightly stronger property for distributing a later
over an existential quantifier.

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 happened for example in <[i:=x]>∅, where simpl unfold insert (despite
it being declared simpl never) because ∅ reduces to a constructor.

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