theorem
Hex.List.nodup_subset_length_le
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(h₁ : l₁.Nodup)
(hsub : l₁ ⊆ l₂)
:
A duplicate-free list contained in another list is no longer than it.
A duplicate-free list contained in another list is no longer than it.