simp only [Var.openList]
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ (V ∘ Var.openList j (List.map free_ zs)) (bound_ i) =
    match
      if i + 1 < j + 1 then bound_ (i + 1)
      else
        if x : i + 1 - (j + 1) < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - (j + 1)]
        else bound_ (i + 1 - (j + 1) - (List.map free_ zs).length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)