intro x a1
v u : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v ∈ xs → u ∉ binders
⊢ ∀ x ∈ xs, decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) 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
⊢ decide (x ∈ binders) = ((fun v => decide (v ∈ binders)) ∘ fun x => if v = x then u else x) x