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

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