case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  intro x
  split_ifs <;> tauto
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ v ∉ List.map (fun x => if v = x then t else x) xs
no goals