jonaprieto/agda-prop

Contraposition

jonaprieto opened this issue · 0 comments

We require some theorems about contraposition:

   p => q
-------
¬ q => ¬ p

¬ q => ¬ p
----------
    p => q

(p => q) <==> (¬ q => ¬ p)

In the implication module is present the second one of these.