Well-quasi-orders: finite bases and Higman's lemma

The finite-basis property of well-quasi-orders — every upward-closed set is the union of finitely many principal filters — stated relation-style, and Higman's lemma: over a finite alphabet the sublist order on List α is a well-quasi-order, specialising mathlib's Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ to equality.

theorem WellQuasiOrdered.exists_finset_eq_biUnion {α : Type u_1} {r : α → α → Prop} [IsPartialOrder α r] (hr : WellQuasiOrdered r) {s : Set α} (hs : ∀ ⦃a b : α⦄, r a b → a ∈ s → b ∈ s) : ∃ (F : Finset α), s = ⋃ a ∈ F, {b : α | r a b}

Finite-basis property of a well-quasi-ordered partial order: every upward-closed set is the union of the principal filters of its finitely many minimal elements.

instance List.instIsPartialOrderSublist_linglib {α : Type u_1} : IsPartialOrder (List α) fun (l₁ l₂ : List α) => l₁.Sublist l₂

theorem List.wellQuasiOrdered_sublist {α : Type u_1} [Finite α] : WellQuasiOrdered fun (l₁ l₂ : List α) => l₁.Sublist l₂

Higman's lemma [Hig52]: for a finite type α the sublist order on List α is a well-quasi-order — every infinite sequence of lists has an earlier term that is a sublist of a later one.