∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : Preorder M]
  (motive : (x : List M) → (∀ x_1 ∈ x, 0 < x_1) → x ≠ [] → Prop) (x : List M) (x_1 : ∀ x_1 ∈ x, 0 < x_1) (x_2 : x ≠ []),
  (∀ (x : ∀ x ∈ [], 0 < x) (h : [] ≠ []), motive [] x h) →
    (∀ (b : M) (h : ∀ x ∈ [b], 0 < x) (x : [b] ≠ []), motive [b] h x) →
      (∀ (a b : M) (l : List M) (hl₁ : ∀ x ∈ a :: b :: l, 0 < x) (x : a :: b :: l ≠ []), motive (a :: b :: l) hl₁ x) →
        motive x x_1 x_2