This module contains the Bool simplifying part of the bv_normalize simp set.

theorem Std.Tactic.BVDecide.Normalize.Bool.not_xor (a b : Bool) : (!decide ((a ^^ b) = (a == b))) = true

theorem Std.Tactic.BVDecide.Normalize.Bool.or_elim (a b : Bool) : (a || b) = !(!a && !b)

theorem Std.Tactic.BVDecide.Normalize.Bool.and_left (lhs rhs : Bool) (h : (lhs && rhs) = true) : lhs = true

theorem Std.Tactic.BVDecide.Normalize.Bool.and_right (lhs rhs : Bool) (h : (lhs && rhs) = true) : rhs = true