simp only [toIsBoundAux]
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ → u ∉ binders
⊢ toIsBoundAux binders (def_ a✝¹ a✝) = toIsBoundAux binders (def_ a✝¹ (List.map (fun x => if v = x then u else x) a✝))
case def_
v u : VarName
a✝¹ : DefName
a✝ : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ a✝ → u ∉ binders
⊢ 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✝))