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