∀ {α : Type u_1} (motive : (l : List α) → l ⊆ [] → Prop) (l : List α) (h : l ⊆ []),
  (∀ (h : [] ⊆ []), motive [] h) →
    (∀ (head : α) (tail : List α) (h : head :: tail ⊆ []), motive (head :: tail) h) → motive l h