Normalization theorems for the grind tactic.

We are also going to use simproc's in the future.

theorem Lean.Grind.iff_eq (p : Prop) (q : Prop) : (p ↔ q) = (p = q)

theorem Lean.Grind.eq_true_eq (p : Prop) : (p = True) = p

theorem Lean.Grind.eq_false_eq (p : Prop) : (p = False) = ¬p

theorem Lean.Grind.not_eq_prop (p : Prop) (q : Prop) : (¬p = q) = (p = ¬q)

theorem Lean.Grind.imp_eq (p : Prop) (q : Prop) : (p → q) = (¬p ∨ q)

theorem Lean.Grind.not_and (p : Prop) (q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q)

theorem Lean.Grind.not_ite {p : Prop} : ∀ {x : Decidable p} (q r : Prop), (¬if p then q else r) = if p then ¬q else ¬r

theorem Lean.Grind.not_forall {α : Sort u_1} (p : α → Prop) : (¬∀ (x : α), p x) = ∃ (x : α), ¬p x

theorem Lean.Grind.not_exists {α : Sort u_1} (p : α → Prop) : (¬∃ (x : α), p x) = ∀ (x : α), ¬p x

theorem Lean.Grind.cond_eq_ite {α : Type u_1} (c : Bool) (a : α) (b : α) : (bif c then a else b) = if c = true then a else b

theorem Lean.Grind.Nat.lt_eq (a : Nat) (b : Nat) : (a < b) = (a + 1 ≤ b)

theorem Lean.Grind.Int.lt_eq (a : Int) (b : Int) : (a < b) = (a + 1 ≤ b)