Module prop::imply

Tactics for Logical IMPLY.

Functions

absurd	false => a.
chain	((a ∧ b) => c => a => (b => c)).
double_neg	(a => b) => ¬¬a => ¬¬b.
flip_neg_left	(¬a => b) => (¬b => a).
flip_neg_right	(¬b => a) => (¬a => b).
from_or	(¬a ∨ b) => (a => b).
id	a => a.
in_left_arg	(a => b) ∧ (a = c) => (c => b).
in_right_arg	(a => b) ∧ (b = c) => (a => c).
modus_ponens	(a => b) ∧ a => b
modus_tollens	a => b => ¬b => ¬a.
reorder_args	a => (b => c) => b => (a => c)
rev_double_neg	(¬¬a => ¬¬b) => a => b.
rev_modus_ponens	(b => a) ∧ ¬a => ¬b.
rev_modus_tollens	¬b => ¬a => a => b.
to_or	(a => b) => (¬a ∨ b).
transitivity	a => b ∧ b => c => a => c.