case nil =>
  funext v
  simp
  simp only [shiftList]
  cases v
  case _ x =>
    simp only [Var.openList]
  case _ i =>
    simp only [Var.openList]
    split
    case _ c1 =>
      rfl
    case _ c1 =>
      simp
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])
no goals