case eq_ x y =>
  simp
  constructor
  case left | right =>
    intro a1 a2
    subst a1
    contradiction
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) = eq_ x y
no goals