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