case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  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) =
    shift D V d (Var.openList (j + 1) (List.map free_ zs) (bound_ i))
no goals