simp only [Var.openList]
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))
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
      (if i + 1 < 0 then bound_ (i + 1)
      else
        if x : i + 1 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[i + 1 - 0]
        else bound_ (i + 1 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V
      (if i < 0 then bound_ i
      else
        if x : i - 0 < (List.map free_ tl).length then (List.map free_ tl)[i - 0]
        else bound_ (i - 0 - (List.map free_ tl).length + 0))