case succ i =>
    simp only [shift]
    simp only [Var.openList]
    simp
    split
    case _ c1 =>
      have s1 : i + 1 < j + 1
      linarith
      simp only [if_pos s1]
    case _ c1 =>
      have s1 : ¬ i + 1 < j + 1
      linarith
      simp only [if_neg s1]
      split
      case _ c2 =>
        simp
      case _ c2 =>
        simp
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d (bound_ (i + 1)) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ (i + 1)))
case h_3
D : Type
V : VarAssignment D
j : ℕ
zs : List String
d : D
i : ℕ
x✝ : Var
i✝ : ℕ
heq✝ :
  (if i < j then bound_ (i + 1)
    else if h : i - j < zs.length then free_ (zs.get ⟨i - j, ⋯⟩) else bound_ (i - j - zs.length + (j + 1))) =
    bound_ i✝.succ
⊢ V (Var.openList j (List.map free_ zs) (bound_ i)) = V (bound_ i✝)