∀ {α : Type u_1} (motive : Batteries.DList α → Sort u_2) (f : List α → List α)
  (invariant : ∀ (l : List α), f l = f [] ++ l)
  (h_1 :
    (f : List α → List α) →
      (invariant : ∀ (l : List α), f l = f [] ++ l) → motive { apply := f, invariant := invariant }),
  (match { apply := f, invariant := invariant } with
    | { apply := f, invariant := invariant } => h_1 f invariant) =
    h_1 f invariant