cases i
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
case zero
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

case succ
zs : List String
X : String
vs : List Var
j n✝ : ℕ
a1 : bound_ (n✝ + 1) ∈ vs
h1 : Var.lc_at j (bound_ (n✝ + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (n✝ + 1)) = bound_ (n✝ + 1)