case _ i =>
  simp only [isFree] at a1
  cases a1
  case _ a1_left a1_right =>
    contradiction
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ (bound_ i).isFree
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
no goals