simp
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V
      (Var.close j (free_ z)
        (if i < j then bound_ i
        else if x : i - j < [free_ z].length then [free_ z][i - j] else bound_ (i - j - [free_ z].length + j)))
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : free_ z ∉ vs
i : ℕ
a1 : bound_ i ∈ vs
h2 : i < j
⊢ V (bound_ i) =
    V (Var.close j (free_ z) (if i < j then bound_ i else if i - j = 0 then free_ z else bound_ (i - j - 1 + j)))