split
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (if i + 1 < j + 1 then bound_ (i + 1) else bound_ (i + 1 + 1)) =
    V (if i < j then bound_ i else bound_ (i + 1))
case inl
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
h✝ : i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1)) = V (if i < j then bound_ i else bound_ (i + 1))

case inr
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
h✝ : ¬i + 1 < j + 1
⊢ shift D V d (bound_ (i + 1 + 1)) = V (if i < j then bound_ i else bound_ (i + 1))