split_ifs
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
⊢ shift D V d (if x = z then bound_ (j + 1) else free_ x) = V (if x = z then bound_ j else free_ x)
case pos
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
h✝ : x = z
⊢ shift D V d (bound_ (j + 1)) = V (bound_ j)

case neg
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
x : String
h✝ : ¬x = z
⊢ shift D V d (free_ x) = V (free_ x)