{α : Type u_1} →
  (motive : α → Batteries.DList α → Sort u_2) →
    (x : α) →
      (x_1 : Batteries.DList α) →
        ((a : α) →
            (f : List α → List α) → (h : ∀ (l : List α), f l = f [] ++ l) → motive a { apply := f, invariant := h }) →
          motive x x_1