cases a1
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isFree
⊢ free_ x ∈ vs
case intro
X : String
vs : List Var
x : String
left✝ : free_ x ∈ vs
right✝ : (free_ x).isFree
⊢ free_ x ∈ vs