case _ i =>
  cases i
  case zero =>
    conv =>
      rhs
      simp only [shift]
    simp only [Var.close]
    simp
    simp only [shift]
  case succ i =>
    conv =>
      rhs
      simp only [shift]
      simp
      simp only [Var.close]
    simp only [Var.close]
    split
    case _ c1 =>
      have s1 : i < j
      linarith
      simp only [if_pos s1]
      simp only [shift]
    case _ c1 =>
      simp at c1
      have s1 : ¬ i < j
      linarith
      simp only [if_neg s1]
      simp only [shift]
D : Type
V : VarAssignment D
j : ℕ
z : String
d : D
i : ℕ
⊢ shift D V d (Var.close (j + 1) (free_ z) (bound_ i)) = shift D (V ∘ Var.close j (free_ z)) d (bound_ i)
no goals