specialize h fun i => if h : i < x.vars then f ⟨i, h⟩ else false
x : BoolExpr Nat
h : x.unsat
f : Fin x.vars → Bool
⊢ eval f x.attach = false
x : BoolExpr Nat
f : Fin x.vars → Bool
h : eval (fun i => if h : i < x.vars then f ⟨i, h⟩ else false) x = false
⊢ eval f x.attach = false