case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  intro x a1 a2 a3
  by_cases c1 : v = x ∧ x ∉ binders
  case pos =>
    cases c1
    case intro c1_left c1_right =>
      subst c1_left
      exact c1_right
  case neg =>
    simp at c1
    specialize a2 c1
    subst a2
    contradiction
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : t ∉ xs
⊢ t ∈ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs ∧ t ∉ binders → v ∉ binders
no goals