Module prop::not

Tactics for Logical NOT.

Functions

• absurd
  ¬a ⋀ a => b.
• double
  a => ¬¬a.
• eq
  (a == b) => (¬a == ¬b).
• rev_double
  ¬¬a => a.
• rev_double_excm
  ¬¬a => a.
• rev_triple
  ¬¬¬a => ¬a.