simp [normalize, interp]
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize (bexpr.not b) = true ↔ interp (bexpr.not b)
case not
b : bexpr
ih : normalize b = true ↔ interp b
⊢ normalize b = false ↔ ¬interp b