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 + 1) ∈ vs
h1 : Var.lc_at j (bound_ (i + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
no goals