case _ hd tl ih =>
  funext v
  simp
  simp only [shiftList]
  cases v
  case _ x =>
    simp only [shift]
    simp only [← ih]
    simp only [Var.openList]
    simp
  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)
⊢ V ∘ Var.openList 0 (List.map free_ (hd :: tl)) = shiftList D V (List.map (V ∘ free_) (hd :: tl))
no goals