fact: Fixpoint all_permutations_aux (l : list A) (n : nat) {struct n} : list (list A) := match n with | O => nil :: nil | S n1 => flat_map (fun p : A * list A => map (cons (fst p)) (all_permutations_aux (snd p) n1)) ( split_one l) end.
imports: List ListAux