• Ralf Jung's avatar
    Merge branch 'double_negation' into 'master' · 62a55d05
    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
_CoqProject 2.65 KB