∀ {α : Type u_1} (motive : (l : List α) → Quot.mk (⇑(List.isSetoid α)) l ≠ 0 → Prop) (l : List α)
  (hl : Quot.mk (⇑(List.isSetoid α)) l ≠ 0),
  (∀ (h : Quot.mk ⇑(List.isSetoid α) [] ≠ 0), motive [] h) →
    (∀ (a : α) (l : List α) (x : Quot.mk (⇑(List.isSetoid α)) (a :: l) ≠ 0), motive (a :: l) x) → motive l hl