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