induction xs
D : Type
V : VarAssignment D
xs : List String
⊢ V ∘ Var.openList 0 (List.map free_ xs) = shiftList D V (List.map (V ∘ free_) xs)
case nil
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])

case cons
D : Type
V : VarAssignment D
head✝ : String
tail✝ : List String
tail_ih✝ : V ∘ Var.openList 0 (List.map free_ tail✝) = shiftList D V (List.map (V ∘ free_) tail✝)
⊢ V ∘ Var.openList 0 (List.map free_ (head✝ :: tail✝)) = shiftList D V (List.map (V ∘ free_) (head✝ :: tail✝))