∀ {α : Type u_1} (x : α) {l₁ : List α} (motive : (l₁_1 : List α) → l₁_1.Sublist (x :: l₁) → Prop) (l₁_1 : List α)
  (s : l₁_1.Sublist (x :: l₁)),
  (∀ (l₁_2 : List α) (s : l₁_2.Sublist l₁), motive l₁_2 ⋯) →
    (∀ (l₁_2 : List α) (s : l₁_2.Sublist l₁), motive (x :: l₁_2) ⋯) → motive l₁_1 s