∀ (α : Type u_1) (p : α → Prop) (motive : (x : List α) → (∀ ⦃x_1 : α⦄, x_1 ∈ x → p x_1) → Prop) (x : List α)
  (x_1 : ∀ ⦃x_1 : α⦄, x_1 ∈ x → p x_1),
  (∀ (hL' : ∀ ⦃x : α⦄, x ∈ [] → p x), motive [] hL') →
    (∀ (head : α) (l' : List α) (hL' : ∀ ⦃x : α⦄, x ∈ head :: l' → p x), motive (head :: l') hL') → motive x x_1