split
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 < j then bound_ (i + 1)
      else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1)) with
    | free_ x => V (free_ x)
    | bound_ 0 => d
    | bound_ i.succ => V (bound_ i)
case h_1
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝¹ : Var
x✝ : String
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    free_ x✝
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (free_ x✝)

case h_2
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ 0
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = d

case h_3
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
i✝ : ℕ
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ i✝.succ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (bound_ i✝)