theorem List.Chain'.nodup_of_trans_irreflex {α : Type u_1} {l : List α} {R : α → α → Prop} (R_trans : Transitive R) (R_irrefl : Irreflexive R) (h_chain : List.Chain' R l) : l.Nodup

instance List.finiteNodupList {α : Type u_1} [DecidableEq α] [Finite α] : Finite { l : List α // l.Nodup }

Equations

• ⋯ = ⋯

theorem List.chains_finite {α : Type u_1} {R : α → α → Prop} [DecidableEq α] [Finite α] (R_trans : Transitive R) (R_irrefl : Irreflexive R) : Finite { l : List α // List.Chain' R l }