Module prop::and

Tactics for Logical AND.

Functions

• assoc
  (a ∧ b) ∧ c => a ∧ (b ∧ c).
• distrib
  a ∧ (b ∨ c) => (a ∧ b) ∨ (a ∧ c).
• eq_left
  (a == b) => (a ∧ c) == (b ∧ c).
• eq_left_false
  ¬c => (a ∧ c) == (b ∧ c).
• eq_right
  (a == b) => (c ∧ a) == (c ∧ b).
• eq_right_false
  ¬c => (c ∧ a) == (c ∧ b).
• exc_both
  (¬a ∧ ¬b) ∧ (a ∨ b) => false
• exc_left
  ¬a ∧ (a ∨ b) => b.
• exc_right
  ¬b ∧ (a ∨ b) => a
• false_arg
  (false ∧ a) => false.
• from_de_morgan
  ¬(a ∨ b) => (¬a ∧ ¬b).
• from_imply
  ¬(a => b) => (a ∧ ¬b).
• fst
  (a ∧ b) => a.
• in_left
  Makes it easier to traverse.
• in_left_arg
  (a ∧ b) ∧ (a => c) => (c ∧ b).
• in_right
  Makes it easier to traverse.
• in_right_arg
  (a ∧ b) ∧ (b => c) => (a ∧ c).
• paradox
  (a ∧ ¬a) => false.
• paradox_e
  (¬¬a ∧ ¬a) => false.
• rev_assoc
  a ∧ (b ∧ c) => (a ∧ b) ∧ c.
• rev_distrib
  (a ∧ b) ∨ (a ∧ c) => a ∧ (b ∨ c).
• rev_eq_left_true
  ((a ∧ c) == (b ∧ c)) ∧ c => (a == b).
• rev_eq_right_true
  ((c ∧ a) == (c ∧ b)) ∧ c => (a == b).
• snd
  (a ∧ b) => b.
• symmetry
  a ∧ b => b ∧ a.
• to_de_morgan
  (¬a ∧ ¬b) => ¬(a ∨ b).
• to_eq_neg
  (¬a ∧ ¬b) => (a == b).
• to_eq_pos
  (a ∧ b) => (a == b).
• to_imply
  (a ∧ ¬b) => ¬(a => b).
• to_or
  (a ∧ b) => (a ∨ b).
• true_arg
  (true ∧ a) => a.