simp only [Var.boundVarSet]
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).boundVarSet
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isBound
⊢ bound_ i ∈ vs ∧ bound_ i ∈ {bound_ i}