case _ x =>
  simp only [Var.openList]
zs : List String
X : String
vs : List Var
j : ℕ
x : String
a1 : free_ x ∈ vs
h1 : Var.lc_at j (free_ x)
⊢ Var.openList j (List.map free_ zs) (free_ x) = free_ x
no goals