induction x with
| literal a => rfl
| const b => rfl
| not x ih => simp [eval, ih, toBoolExpr]
| gate g x y ihx ihy => simp [eval, ihx, ihy, toBoolExpr]
x : BoolExprNat
f : List Bool
⊢ BoolExpr.eval (fun x => f.getD x false) x.toBoolExpr = eval f x
no goals