Chain

theorem List.IsChain.nodup_of_trans_irreflex {α : Type u_1} {l : List α} {R : α → α → Prop} (R_trans : IsTrans α R) (R_irrefl : Std.Irrefl R) (h_chain : IsChain R l) : l.Nodup

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

theorem List.chains_finite {α : Type u_1} {R : α → α → Prop} [Finite α] (R_trans : IsTrans α R) (R_irrefl : Std.Irrefl R) : Finite { l : List α // IsChain R l }