simp only [Var.lc_at] at h1
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0