case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  simp only [List.map_eq_self_iff]
  simp
v : VarName
X : DefName
xs : List VarName
⊢ def_ X (List.map (fun x => if v = x then v else x) xs) = def_ X xs
no goals