case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp at h2
  simp only [List.map_eq_map_iff] at h2
  intro a1
  specialize h2 v a1
  simp at h2
  tauto
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 :
  BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) xs) =
    BoolFormula.def_ X (List.map (fun v => decide (v ∈ binders)) (List.map (fun x => if v = x then u else x) xs))
⊢ v ∈ xs → u ∉ binders
no goals