-
Ralf Jung authored
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
62a55d05