case _ a2_left a2_right =>
  subst a2_right
  simp only [isBound]
  simp
  exact a2_left
v : Var
X : String
vs : List Var
a1 : ∃ a ∈ vs, v ∈ a.boundVarSet
i : ℕ
a2_left : bound_ i ∈ vs
a2_right : v = bound_ i
⊢ v ∈ vs ∧ v.isBound
no goals