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