simp only [toIsBoundAux] at h2
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) a✝) =
    BoolFormula.def_ a✝¹ (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) a✝))
⊢ v ∈ a✝ → u ∉ binders