theorem
List.nodup_subset_length_le
{α : Type u_1}
[DecidableEq α]
{l₁ l₂ : List α}
(h₁ : l₁.Nodup)
(hsub : l₁ ⊆ l₂)
:
A Nodup list contained in another list is no longer than it. Replaces uses
of Batteries' Subperm API (subperm_of_subset/Subperm.length_le), which
core lacks; unlike the declarations above, this name is local to Hex.