cases v
case h
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
v : Var
⊢ shift D V d (Var.close (j + 1) (free_ z) v) = shift D (V ∘ Var.close j (free_ z)) d v
case h.free_
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
a✝ : String
⊢ shift D V d (Var.close (j + 1) (free_ z) (free_ a✝)) = shift D (V ∘ Var.close j (free_ z)) d (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
a✝ : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ a✝)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ a✝)