simp
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ V (bound_ i) =
    if
        (if i + 1 < 0 then bound_ (i + 1)
          else
            if x : i + 1 - 0 < [free_ z].length then [free_ z][i + 1 - 0]
            else bound_ (i + 1 - 0 - [free_ z].length + 0)) =
          free_ z then
      d
    else
      V
        (if i + 1 < 0 then bound_ (i + 1)
        else
          if x : i + 1 - 0 < [free_ z].length then [free_ z][i + 1 - 0] else bound_ (i + 1 - 0 - [free_ z].length + 0))
no goals