simp only [isFree] at a1
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isFree
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet