simp [eval, toBoolExpr, eval_ofFn]
k : Nat
x✝ : BoolExprNat
f : Fin k → Bool
x : BoolExprNat
⊢ eval (List.ofFn f) x.not = BoolExpr.eval (fun i => if h : i < k then f ⟨i, h⟩ else false) x.not.toBoolExpr
no goals