Module prop::not

source · [−]
Expand description

Tactics for Logical NOT.

Functions

absurd

¬a ⋀ a => b.

double

a => ¬¬a.

rev_double

¬¬a => a.

rev_triple

¬¬¬a => ¬a.