case _ i =>
  cases i
  case zero =>
    simp only [Var.lc_at] at h1
    simp only [Var.openList]
    simp only [if_pos h1]
  case succ i =>
    simp only [Var.lc_at] at h1
    simp only [Var.openList]
    simp only [if_pos h1]
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ i ∈ vs
h1 : Var.lc_at j (bound_ i)
⊢ Var.openList j (List.map free_ zs) (bound_ i) = bound_ i
no goals