simp [normalize, interp, ← iha, ← ihb]
case imp
a b : bexpr
iha : normalize a = true ↔ interp a
ihb : normalize b = true ↔ interp b
⊢ normalize (imp a b) = true ↔ interp (imp a b)
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