rw [eval_attach] at h
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => f ↑i) x.attach = false
⊢ eval f x = false
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ eval f x = false