case intro h2_left h2_right =>
  intros a1
  cases a1
  case inl a1 =>
    subst a1
    simp at h2_left
    tauto
  case inr a1 =>
    subst a1
    simp at h2_right
    tauto
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : y ∈ binders ↔ (if v = y then u else y) ∈ binders
⊢ v = x ∨ v = y → u ∉ binders
no goals