∀ {ι : Type u_1} {f : ι → Ordinal.{u_2} → Ordinal.{u_2}} {a b : Ordinal.{u_2}}
  (motive : (∃ l, b < List.foldr f a l) → Prop) (x : ∃ l, b < List.foldr f a l),
  (∀ (l : List ι) (hl : b < List.foldr f a l), motive ⋯) → motive x