simp_all
case w
x : BoolExpr Nat
f : Nat → Bool
h : eval (fun i => if h : i < x.vars then f ↑⟨i, h⟩ else false) x = false
⊢ ∀ (i : Nat), i < x.vars → f i = if h : i < x.vars then f ↑⟨i, h⟩ else false
no goals