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

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