intro x
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ ∀ x ∈ xs, ¬(if v = x then t else x) = v
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
x : VarName
⊢ x ∈ xs → ¬(if v = x then t else x) = v