Library Obs.list_tools

RIS.list tools : Toolbox of list operators and their properties.

Require Import notations Psatz Bool.
Require Export List.
Export ListNotations.
Set Implicit Arguments.
Global Hint Unfold Basics.compose : core.

Lists

Notations

We associate the traditional containment symbol to list inclusion.

Infix " ⊆ " := incl (at level 80).

We use the following symbol to denote the membership predicate.

Infix " ∈ " := In (at level 60).

We'll write P :> l for the list l where we've removed elements that do not satisfy the boolean predicate P.

Infix " :> " := filter (at level 50).

The size of a list is its length.

Global Instance SizeList {A} : Size (list A) := (@length A).

Remark SizeLength {A : Type} (l : list A) : length l = ⎢l ⎥.
Remark SizeCons {A:Type} (a : A) (l : list A) : ⎢a ::l ⎥ = S ⎢l ⎥.
Remark SizeNil {A:Type} : ⎢@nil A ⎥ = 0.
Remark SizeApp {A:Type} (l m : list A) : ⎢l ++m ⎥ = ⎢l ⎥+⎢m ⎥.
Remark SizeMap {A B:Type} (l : list A) (f : A → B): ⎢map f l ⎥ = ⎢l ⎥.
Global Hint Rewrite @SizeLength @SizeCons @SizeNil @SizeApp @SizeMap: simpl_typeclasses.

Induction principles

Induction principle for lists in the reverse order.

Lemma rev_induction {A} (P : list A → Prop) :
P [] → (∀ a l, P l → P (l ++[a ])) → ∀ l, P l.

Strong induction on the length of a list.

Lemma len_induction {A} (P : list A → Prop) :
P [] → (∀ a l, (∀ m, ⎢m ⎥ ≤ ⎢l ⎥ → P m ) → P (a ::l)) → ∀ l, P l.

Strong induction on the length of a list, taken in the reverse order.

Lemma len_rev_induction {A} (P : list A → Prop) :
P [] → (∀ a l, (∀ m, ⎢m ⎥ ≤ ⎢l ⎥ → P m ) → P (l ++[a ])) → ∀ l, P l.

General lemmas

A list is not empty if and only if it has a last element.

Lemma not_nil_add {A} (v : list A) : v ≠ [] ↔ ∃ u l , v = u ++[l ].

A list is either empty or can be decomposed with its last element apparent.

Lemma nil_or_last {A} (v : list A) : {v = []} + {∃ a v', v = v'++[a ]}.

If the list l++a::l' is duplicate free, so are l and l'.

Lemma NoDup_remove_3 {A} (l l' : list A) (a : A) :
NoDup (l ++ a :: l') → NoDup l ∧ NoDup l'.

Filtering a concatenation is the same as concatenating filters.

Lemma filter_app {A} (f : A → bool) (l m : list A) :
f :> (l ++m ) = f :> l ++ f :> m.

Filtering reduces the length of the list.

Lemma filter_length {A} (f : A → bool) l :
⎢f :> l ⎥ ≤ ⎢l ⎥ .

The following lemma give a more precise description.

Lemma filter_length_eq {A} (f : A → bool) l :
⎢f :> l ⎥ + ⎢(fun x ⇒ negb (f x)) :> l ⎥ = ⎢l ⎥ .

If there is an element in l not satisfying f, then f :> l is strictly smaller than l.

Lemma filter_length_lt {A} (f : A → bool) (l : list A) a :
a ∈ l → f a = false → ⎢f :> l ⎥<⎢l ⎥.

filter and map commute.

Lemma filter_map {A B} (f : A → bool) (g : B → A) l :
f :> (map g l ) = map g ((fun x ⇒ f (g x)) :> l).

filter only depends on the values of the filtering function, not its implementation.

Lemma filter_ext_In {A} (f g : A → bool) l :
(∀ x, x ∈ l → f x = g x ) → f :> l = g :> l.

Lemma filter_ext {A} (f g : A → bool) l :
(∀ x, f x = g x ) → f :> l = g :> l.

Filtering with the predicate true does not modify the list.

Lemma filter_true {A} (l : list A) :
(fun _ ⇒ true ) :> l = l.

Filtering preserves the property NoDup (absence of duplicates).

Lemma filter_NoDup {A} (f : A → bool) l :
NoDup l → NoDup (f :> l).

A filtered list P :> l is empty if and only if P x is false for every element x∈l.

Lemma filter_nil {A} (P : A → bool) l :
P :>l = [] ↔ ∀ a, a ∈ l → P a = false.

If two concatenations are equal, and if the two initial factors have the same length, then the factors are equal.

Lemma length_app {A} (l1 l2 m1 m2 : list A) :
⎢l1 ⎥ = ⎢m1 ⎥ → l1 ++l2 = m1 ++m2 → l1 = m1 ∧ l2 = m2.

If two concatenations are equal, and if the two final factors have the same length, then the factors are equal.

Lemma length_app_tail {A} (l1 l2 m1 m2 : list A) :
⎢l2 ⎥ = ⎢m2 ⎥ → l1 ++l2 = m1 ++m2 → l1 = m1 ∧ l2 = m2.

If two concatenations are equal, and the first initial factor is smaller than the second one, we can find a unifying factor w.

Lemma app_eq_app_length {A : Set} (u1 u2 v1 v2 : list A) :
u1 ++u2 = v1 ++ v2 → ⎢u1 ⎥ ≤ ⎢v1 ⎥ → ∃ w , v1 = u1 ++w ∧ u2 = w ++v2.

If two concatenations are equal, we can always find a unifying factor.

Lemma Levi {A:Set} (u1 u2 v1 v2 : list A) :
u1 ++u2 = v1 ++v2 → ∃ w , (u1 =v1 ++w ∧ v2 =w ++u2 ) ∨ (v1 =u1 ++w ∧ u2 =w ++v2 ).

This next lemma makes the unifying factor unambiguous.

Lemma Levi_strict {A:Set} (u1 u2 v1 v2 : list A) :
  u1 ++u2 = v1 ++v2 → (u1 = v1 ∧ u2 = v2 )
                    ∨ ∃ a w , (u1 =v1 ++a ::w ∧ v2 =a ::w ++u2 ) ∨ (v1 =u1 ++a ::w ∧ u2 =a ::w ++v2 ).

Ltac levi u v :=
  let a := fresh "a" in
  let w := fresh "w" in
  let h := fresh "h" in
  let E1 := fresh "E" in
  let E2 := fresh "E" in
  assert (h:u=v);
  [auto
  |destruct (Levi_strict h) as [E1|(a&w&[E1|E1])];
   destruct E1 as (E1&E2);repeat (rewrite E1 in × || rewrite E2 in × )].

Tactic Notation "levi" hyp(h) :=
  let a := fresh "a" in
  let w := fresh "w" in
  let E1 := fresh "E" in
  let E2 := fresh "E" in
  destruct (Levi_strict h) as [E1|(a&w&[E1|E1])];
  destruct E1 as (E1&E2);repeat (rewrite E1 in × || rewrite E2 in × ).

If the concatenation of two lists is duplication free, then so are they.

Lemma NoDup_app_inv {X:Set} : ∀ (l m : list X),
NoDup (l ++m) → NoDup l ∧ NoDup m.

If l and m don't share any element, then if both of them don't have duplication their concatenation won't either.

Lemma NoDup_app {X : Set} l m:
(∀ a : X, a ∈ l → ¬ a ∈ m ) → NoDup l → NoDup m → NoDup (l ++m).

If the boolean predicate forallb f l is false, then me may extract a counter-example, that is an element in the list l where the predicate f is false.

Lemma forallb_false_exists {A} f (l:list A) :
forallb f l = false ↔ ∃ a , a ∈ l ∧ f a = false.

l appears in the list concat m exactly when there is a list L in m such that l appears in L.

Lemma in_concat {A : Set} l (m : list (list A)) :
l ∈ concat m ↔ ∃ L , L ∈ m ∧ l ∈ L.

If map f m can be split into l1++l2, then we may split l into m1++m2 accordingly.

Lemma map_app_inverse {A B} (f : A → B) m l1 l2 :
map f m = l1 ++ l2 → ∃ m1 m2 , l1 = map f m1 ∧ l2 = map f m2 ∧ m = m1 ++ m2.

lift_prod f is the pointwise extension of the binary operation f over A into a binary operation over list A.

Definition lift_prod {A} (f : A → A → A) : list A → list A → list A :=
fun l m ⇒ flat_map (fun a ⇒ map (f a) m) l.

Lemma lift_prod_spec {A} f (l m : list A) :
∀ c, c ∈ lift_prod f l m ↔ ∃ a b , a ∈ l ∧ b ∈ m ∧ c = f a b.

Lemma incl_map {A B:Set} (f : A → B) l m : l ⊆ map f m → ∃ n , l = map f n ∧ n ⊆ m.

Lists of pairs

We introduce some notations for lists of pairs: prj1 l is the list obtained by applying pointwise to l the function fun (x,y) ⇒ x.

Notation prj1 := (map fst).

Similarly, prj2 l is the list obtained by applying pointwise to l the function fun (x,y) ⇒ y.

Notation prj2 := (map snd).

If the a projection of l is equal to a projection of m, then they have the same length.

Lemma proj_length {A B C} (l : list (A ×B)) (m:list (B ×C)) : prj2 l = prj1 m → ⎢l ⎥=⎢m ⎥.

Combine

Section combine.
  Context {A B : Set}.
  Context {l1 l3 : list A} {l2 l4: list B} {l: list (A ×B)}.
  Hypothesis same_length : ⎢l1 ⎥ = ⎢l2 ⎥.

The combine function can be described by the following recursive definition :

[]⊗l = l⊗[] = [];
(a::l)⊗(b::m)=(a,b)::(l⊗m).

In the following, we will only use l⊗m when l and m have the same length.

Infix "⊗" := combine (at level 50).

The first projection of l1 ⊗ l2 is l1.

Lemma combine_fst : prj1 (l1 ⊗ l2) = l1.

The second projection of l1 ⊗ l2 is l2.

Lemma combine_snd : prj2 (l1 ⊗ l2) = l2.

A combination of concatenations is the concatenation of combinations (assuming the first arguments of both concatenations have the same length).

Lemma combine_app : (l1 ++l3 ) ⊗ (l2 ++l4 ) = l1 ⊗ l2 ++ l3 ⊗ l4.

Every list of pairs can be expressed as the combination of its first and second components.

Lemma combine_split : l = (prj1 l ) ⊗ (prj2 l ).

End combine.
Infix "⊗" := combine (at level 50).

Mix

Section mix.
Context {A B : Set} {s1 s2 s3 s4 : list (A ×B)}.
Hypothesis same_length : ⎢s1 ⎥ = ⎢s2 ⎥.

Given two lists of pairs s1 and s2, the mix of s1 and s2 is the combination of the first projection of s1 with the second projection of s2. We will only use this construct when s1 and s2 have the same length.

  Definition mix (s1 s2 : list (A ×B)) := (prj1 s1 ) ⊗ (prj2 s2 ).
  Infix "⋈" := mix (at level 50).

  Lemma mix_fst : prj1 (s1 ⋈ s2) = prj1 s1.

  Lemma mix_snd : prj2 (s1 ⋈ s2) = prj2 s2.

  Lemma mix_app : (s1 ++s3 ) ⋈ (s2 ++s4 ) = s1 ⋈ s2 ++ s3 ⋈ s4.
End mix.
Infix "⋈" := mix (at level 50).

Flip

Section flip.
Context {A B : Set} {l m : list (A ×B)}.

Flipping a list of pairs amounts to applying pointwise to the list the function fun (x,y) ⇒ (y,x), that is exchanging the order of every pair in the list.

Definition flip {A B} : list (A ×B) → list (B ×A) := map (fun x ⇒ (snd x ,fst x )).
Notation " l ` " := (flip l) (at level 20).

Flip is an involution.

Lemma flip_involutive : l `` = l.

Flip distributes over concatenations.

Lemma flip_app : (l ++m )`=l `++m `.

Flip swaps first and second projections.

Lemma flip_proj1 : prj1 (l `) = prj2 l.

Lemma flip_proj2 : prj2 (l `) = prj1 l.

The pair (a,b) is in l if and only if (b,a) is in l`.

Lemma In_flip a b : (a ,b ) ∈ l ` ↔ (b ,a ) ∈ l.

End flip.
Notation " l ` " := (flip l) (at level 30).

Lists as finite sets

We say that two lists are equivalent if they contain the same elements.

Definition equivalent A l m := ∀ x : A , x ∈ l ↔ x ∈ m.
Infix " ≈ " := equivalent (at level 80).

We now establish that ≈ is a congruence, and that ⊆ is a partial order.

Global Instance equivalent_Equivalence T : Equivalence (@equivalent T).
Global Instance incl_PreOrder T : PreOrder (@incl T).
Global Instance incl_PartialOrder T :
PartialOrder (@equivalent T) (@incl T).

Concatenation preserves both relations.

Global Instance incl_app_Proper T :
  Proper ((@incl T ) ==> (@incl T ) ==> (@incl T )) (@app T).
Global Instance equivalent_app_Proper T :
  Proper ((@equivalent T ) ==> (@equivalent T ) ==> (@equivalent T ))
         (@app T).

The operation of adding an element to a list preserves both relations.

Global Instance incl_cons_Proper T a :
Proper ((@incl T ) ==> (@incl T )) (cons a).
Global Instance equivalent_cons_Proper T a :
Proper ((@equivalent T ) ==> (@equivalent T )) (cons a).

For any function f, the list morphism map f preserves both relations.

Global Instance map_incl_Proper {A B} (f : A → B) :
Proper (@incl A ==> @incl B) (map f).
Global Instance map_equivalent_Proper {A B} (f : A → B) :
Proper (@equivalent A ==> @equivalent B) (map f).

For any boolean predicate f, the filtering map filter f preserves both relations.

Global Instance filter_incl_Proper {A} (f : A → bool) :
Proper (@incl A ==> @incl A) (filter f).
Global Instance filter_equivalent_Proper {A} (f : A → bool) :
Proper (@equivalent A ==> @equivalent A) (filter f).

The lemmas In_incl_Proper and In_equivalent_Proper are completely tautological, but turn out to be useful for technical reasons.

Global Instance In_incl_Proper {A} (x : A): Proper ((@incl A ) ==> Basics.impl) (In x).
Global Instance In_equivalent_Proper {A} (x : A): Proper ((@equivalent A ) ==> iff) (In x).

The operation of reversing a list preserves both relations.

Lemma rev_equivalent {A} (l : list A) : l ≈ rev l.
Global Instance incl_rev_Proper T : Proper ((@incl T ) ==> (@incl T )) (@rev T).
Global Instance equivalent_rev_Proper T : Proper ((@equivalent T ) ==> (@equivalent T )) (@rev T).

The flat_map function preserves both relations.

Global Instance incl_flat_map_Proper A B (f : A → list B) :
Proper ((@incl A ) ==> (@incl B )) (flat_map f).
Global Instance equivalent_flat_map_Proper A B (f : A → list B) :
Proper ((@equivalent A ) ==> (@equivalent B )) (flat_map f).

The lift_prod f function preserves both relations.

Global Instance incl_lift_prod_Proper {A:Set} (f : A → A → A) :
Proper ((@incl _) ==> (@incl _) ==> (@incl _)) (lift_prod f).
Global Instance equivalent_lift_prod_Proper {A:Set} (f : A → A → A) :
Proper ((@equivalent _) ==> (@equivalent _) ==> (@equivalent _)) (lift_prod f).

The following simple facts about inclusion and equivalence are convenient to have in our toolbox.

Lemma incl_nil T (A : list T) : [] ⊆ A.
Lemma incl_app_or T (A B C : list T) : A ⊆ B ∨ A ⊆ C → A ⊆B ++C.
Create HintDb eq_list.
Lemma incl_app_split {A} (l m p : list A) : l ++m ⊆ p ↔ l ⊆ p ∧ m ⊆ p.
Global Hint Resolve incl_appl incl_appr incl_nil app_assoc : eq_list.
Lemma app_idem {A} (l : list A) : l ++ l ≈ l.
Lemma app_comm {A} (l m : list A) : l ++ m ≈ m ++ l.
Lemma incl_split {A} (l m n : list A) :
l ⊆ m ++ n → ∃ l1 l2 , l ≈ l1 ++l2 ∧ l1 ⊆ m ∧ l2 ⊆ n.

More general lemmas

If a boolean predicate f fails to be true for every element of a list l, then there must exists a witnessing element y falsifying f. This is an instance of a classical principle holding constructively when restricted to decidable properties over finite domains.

Lemma forall_existsb {A} (f : A → bool) l :
¬ (∀ x, x ∈ l → f x = true ) → ∃ y , y ∈ l ∧ f y = false.

In forallb f l we may replace f with a function g outputting the same values on the elements of l.

Lemma forallb_ext_In {A} (f g : A → bool) l : (∀ a, a ∈ l → f a = g a ) → forallb f l = forallb g l.

In forallb f l we may replace f with a function g outputting the same values.

Lemma forallb_ext {A} (f g : A → bool) l : (∀ a, f a = g a ) → forallb f l = forallb g l.

For every list l and every function f, l is a fixpoint of map f if and only if every element of l is a fixpoint of f.

Lemma map_eq_id {A} (l : list A) (f : A → A) :
map f l = l ↔ (∀ x, x ∈ l → f x = x ).

fun f ⇒ map f l is bijective, using extensional equality of functions.

Lemma map_bij {A B} (f g : A → B) l : map f l = map g l → ∀ a, a ∈ l → f a = g a.

Lemma map_ext_in_iff (A B : Type) (f g : A → B) (l : list A) :
(∀ a : A, a ∈ l → f a = g a ) ↔ map f l = map g l.

Lemma map_eq_equivalent (A B : Set) (f g : A → B) l m :
l ≈ m → map f m = map g m ↔ map f l = map g l.

We may lift a decomposition of the second (respectively first) component of a list of pairs into a decomposition of the original list.

Lemma split_snd {A B} a (t : list (A × B)) t1 t2 :
prj2 t = t1 ++ a :: t2 → ¬ a ∈ t1 → ∃ k s1 s2 , t = s1 ++(k ,a )::s2 ∧ t1 = prj2 s1 ∧ t2 = prj2 s2.

Lemma split_fst {A B} a (t : list (A × B)) t1 t2 :
prj1 t = t1 ++ a :: t2 → ¬ a ∈ t1 → ∃ k s1 s2 , t = s1 ++(a ,k )::s2 ∧ t1 = prj1 s1 ∧ t2 = prj1 s2.

If n is smaller than the length of u, then u can be split into a prefix of size n, followed by a non-empty list.

Lemma split_word {A} n (u : list A) :
n < ⎢u ⎥ → ∃ x u1 u2 , u = u1 ++x ::u2 ∧ ⎢u1 ⎥ = n.

Subsets of a list

Fixpoint subsets {A : Set} (l : list A) :=
  match l with
  | [] ⇒ [[]]
| a::l ⇒ map (cons a) (subsets l)++subsets l
  end.

Lemma subsets_In {A : Set}(l : list A) :
  ∀ m, m ∈ subsets l → m ⊆ l.

Lemma incl_cons_disj {A : Set} (a : A) m l :
  m ⊆ a :: l → m ⊆ l ∨ ∃ m', m ≈ a ::m' ∧ m' ⊆ l.

Lemma subsets_spec {A : Set} (l : list A) :
  ∀ m, m ⊆ l ↔ ∃ m', m' ∈ subsets l ∧ m ≈ m'.

Lemma subsets_NoDup {A : Set} (k l : list A) :
  NoDup l → k ∈ subsets l → NoDup k.

Pairs

Definition pairs {A B : Set} l r : list (A × B) :=
fold_right (fun a acc ⇒ (map (fun b ⇒ (a ,b )) r )++acc) [] l.

Lemma pairs_spec {A B : Set} l r (a : A) (b : B) : (a ,b ) ∈ pairs l r ↔ a ∈ l ∧ b ∈ r.

Enumerate lists of a certain length

Fixpoint lists_of_length {A} (elts:list A) n :=
  match n with
  | 0 ⇒ [[]]
| S n ⇒ flat_map (fun l ⇒ map (fun e ⇒ e ::l) elts) (lists_of_length elts n)
  end.

Lemma lists_of_length_spec {A} (elts : list A) n l :
  l ∈ lists_of_length elts n ↔ ⎢l ⎥ = n ∧ l ⊆ elts.

Pad a list with an element

Definition pad {A} (e : A) (l : list A) := e ::flat_map (fun a ⇒ [a ;e ]) l.

Lemma pad_contents {A} (e : A) l : pad e l ≈ e ::l.

Sum function

If a1,...,an are elements in A and f is a function from A to nat, then sum f [a1;...;an] is the natural number f a1+...+f an.

Definition sum {A} f (l : list A) := fold_right (fun a acc ⇒ f a + acc) 0 l.

sum f distributes over concatenations.

Lemma sum_app {A} f (l m : list A) : sum f (l ++m) = sum f l + sum f m.

If l is contained in m and has no duplicates, then summing f on l yields a smaller value than summing f on m.

Lemma sum_incl_ND {A} f (l m : list A) :
l ⊆ m → NoDup l → sum f l ≤ sum f m.

If two duplicate-free list are equivalent, then summing f on any of them yields the same result.

Lemma sum_eq_ND {A} f (l m : list A) :
l ≈ m → NoDup l → NoDup m → sum f l = sum f m.

If f is pointwise smaller than g, then the sum sum f l is smaller than sum g l.

Lemma sum_incr {A} f g (l : list A) : (∀ x, f x ≤ g x ) → sum f l ≤ sum g l.

sum f l only depends on the values of f, not its implementation.

Lemma sum_ext {A} f g (l : list A) : (∀ x, f x = g x ) → sum f l = sum g l.

Lemma sum_ext_In {A} f g (l : list A) : (∀ x, x ∈ l → f x = g x ) → sum f l = sum g l.

If h is the pointwise sum of f and g, then sum h l is the sum of sum f l and sum g l.

Lemma sum_add {A} f g h (l : list A) : (∀ x, h x = f x + g x ) → sum h l = sum f l + sum g l.

Lemma sum_add_distr {A} f g (l : list A) : sum f l + sum g l = sum (fun x ⇒ f x + g x) l.

If f is uniformly 0 on the elements of the list l, then sum f l is 0.

Lemma sum_zero_in {A} f (l : list A) : (∀ x, x ∈ l → f x = 0) → sum f l = 0.

Lemma sum_le {A} f g (l : list A) :
(∀ a, a ∈ l → f a ≤ g a ) → sum f l ≤ sum g l.

Lemma sum_lt {A} f g (l : list A) :
(∀ a, a ∈ l → f a ≤ g a ) → (∃ b , b ∈ l ∧ f b < g b ) → sum f l < sum g l.

Lemma sum_filter {A : Set} (P : A → bool) f l : sum f (P :>l) ≤ sum f l.

Enumerate permutations of a list

Section shuffle.
Context {A : Set}.

insert a l generates the list of all possibles lists l1::a++l2 such that l=l1++l2.

  Fixpoint insert (a : A) l :=
    match l with
    | [] ⇒ [[a ]]
| b::l ⇒ (a ::b::l )::(map (cons b) (insert a l))
    end.

shuffles l generates the list of all lists obtained by reordering the elements of l. For instance shuffles [a;b]=[[a;b];[b;a]].

  Fixpoint shuffles l :=
    match l with
    | [] ⇒ [[]]
| a::l ⇒ flat_map (insert a) (shuffles l)
    end.

  Lemma insert_spec a l m :
    m ∈ insert a l ↔ ∃ l1 l2 , l = l1 ++l2 ∧ m = l1 ++a ::l2.

Shuffles of l contain the same elements.

Lemma shuffles_equiv l m : m ∈ shuffles l → l ≈ m.

If l has no duplicates and m is a shuffle of l, then m has no duplicates either.

Lemma shuffles_nodup l m : NoDup l → m ∈ shuffles l → NoDup m.

Shuffles of l have the same length as l.

Lemma shuffles_length l m : m ∈ shuffles l → ⎢l ⎥ = ⎢m ⎥.

If l has no duplicates, then shuffles l contain exactly the lists that are equivalent to l without having any duplicates.

Lemma In_shuffles l m :
NoDup l → m ∈ shuffles l ↔ l ≈ m ∧ NoDup m.

If l1 is a shuffle of l2, then being a shuffle of l1 is equivalent to being a shuffle of l2.

Lemma eq_shuffles l1 l2 : l1 ∈ shuffles l2 → shuffles l1 ≈ shuffles l2.

If l has no duplicates, neither does shuffles l.

  Lemma NoDup_shuffles (l : list A) : NoDup l → NoDup (shuffles l).

End shuffle.

Lemma incl_cons_disj' {A : Set} (a : A) m l :
  NoDup m → m ⊆ a :: l → m ⊆ l ∨ ∃ m', m ≈ a ::m' ∧ m' ⊆ l ∧ NoDup m'.

Lemma all_subsets_nodup {A : Set} (l : list A) :
  NoDup l → ∀ m, m ∈ (flat_map shuffles (subsets l)) ↔ NoDup m ∧ m ⊆ l.