simp [eval, ih, toBoolExpr]
case not
f : List Bool
x : BoolExprNat
ih : BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
⊢ BoolExpr.eval (fun x => f.getD x false) x.not.toBoolExpr = eval f x.not
no goals