case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  case succ i =>
    simp only [shift]
    simp only [← ih]
    simp
    simp only [Var.openList]
    simp
    split
    case _ c1 =>
      have s1 : i < tl.length
      linarith
      simp only [s1]
      simp
    case _ c1 =>
      have s1 : ¬ i < tl.length
      linarith
      simp only [s1]
      simp
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)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ i)
no goals