induction b with
| atom a => cases' a <;> simp [normalize, interp]
| and a b iha ihb => simp [normalize, interp, *]
| or a b iha ihb => simp [normalize, interp, *]
| not b ih =>
  simp [normalize, interp]
  rw [Bool.eq_false_iff]
  tauto
| imp a b iha ihb =>
  simp [normalize, interp, ← iha, ← ihb]
  rw [Bool.eq_false_iff]
  tauto
b : bexpr
⊢ normalize b = true ↔ interp b
no goals