case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  simp only [List.map_eq_self_iff]
  simp
  intro x _ a2 a3
  subst a2
  contradiction
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ def_ X (List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs) = def_ X xs
no goals