cases a1
X : String
vs : List Var
i : ℕ
a1 : bound_ i ∈ vs ∧ False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet
case intro
X : String
vs : List Var
i : ℕ
left✝ : bound_ i ∈ vs
right✝ : False
⊢ bound_ i ∈ vs ∧ bound_ i ∈ (bound_ i).freeVarSet