simp only [← ih]
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)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shiftList D V (List.map (V ∘ free_) tl) (bound_ i)
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)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    (V ∘ Var.openList 0 (List.map free_ tl)) (bound_ i)