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