simp
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
a1 : v ∈ xs
⊢ v ∈ binders ↔ (if v = v then u else v) ∈ binders
case pos
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
a1 : v ∈ xs
⊢ v ∈ binders ↔ u ∈ binders