cases v
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) v
case h.free_
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
a✝ : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ a✝)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
a✝ : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ a✝)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ a✝)