rw [Bool.eq_false_iff]
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a = false ∨ normalize b = true ↔ normalize a = true → normalize b = true
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize a ≠ true ∨ normalize b = true ↔ normalize a = true → normalize b = true