Simplification lemmas for ite.

We don't prove them at logic.lean because it is easier to prove them using the tactic framework.

@[simp]

theorem if_true_right_eq_or (p : Prop) [h : Decidable p] (q : Prop) : (if p then q else True) = (¬p ∨ q)

@[simp]

theorem if_true_left_eq_or (p : Prop) [h : Decidable p] (q : Prop) : (if p then True else q) = (p ∨ q)

@[simp]

theorem if_false_right_eq_and (p : Prop) [h : Decidable p] (q : Prop) : (if p then q else False) = (p ∧ q)

@[simp]

theorem if_false_left_eq_and (p : Prop) [h : Decidable p] (q : Prop) : (if p then False else q) = (¬p ∧ q)