case _ x =>
  simp only [Var.isBound] at a1
  cases a1
  case _ a1_left a1_right =>
    contradiction
X : String
vs : List Var
x : String
a1 : free_ x ∈ vs ∧ (free_ x).isBound
⊢ free_ x ∈ vs ∧ free_ x ∈ (free_ x).boundVarSet
no goals