simp only [Var.openList]
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ (if i + 1 < j then bound_ (i + 1)
    else
      if x : i + 1 - j < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - j]
      else bound_ (i + 1 - j - (List.map free_ zs).length + j)) =
    bound_ (i + 1)