match x with
| literal a => simp [toBoolExpr, List.getD_ofFn]
| const b => rfl
| not x => simp [eval, toBoolExpr, eval_ofFn]
| gate g x y => simp [eval, toBoolExpr, eval_ofFn]
k : Nat
x : BoolExprNat
f : Fin k → Bool
⊢ eval (List.ofFn f) x = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) x.toBoolExpr
no goals