∀ {α : Type u_1} (p : α → Bool)
  (motive :
    (x x_1 : List α) →
      (x_2 : Option α) →
        (x_3 : List α) →
          (∀ x ∈ x_1, p x = false) →
            Option.elim' (x = x_1 ∧ x_3 = []) (fun a => p a = true ∧ x = x_1 ++ a :: x_3) x_2 → Prop)
  (x x_1 : List α) (x_2 : Option α) (x_3 : List α) (x_4 : ∀ x ∈ x_1, p x = false)
  (x_5 : Option.elim' (x = x_1 ∧ x_3 = []) (fun a => p a = true ∧ x = x_1 ++ a :: x_3) x_2),
  (∀ (x : ∀ x ∈ [], p x = false), motive [] [] none [] x ⋯) →
    (∀ (l₁ : List α) (o : α) (l₂ : List α) (x : ∀ x ∈ l₁, p x = false) (left : p o = true) (h₃ : [] = l₁ ++ o :: l₂),
        motive [] l₁ (some o) l₂ x ⋯) →
      (∀ (a : α) (L l₁ : List α) (o : Option α) (l₂ : List α) (h₁ : ∀ x ∈ l₁, p x = false)
          (h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun a_1 => p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o),
          motive (a :: L) l₁ o l₂ h₁ h₂) →
        motive x x_1 x_2 x_3 x_4 x_5