fact: Fixpoint separates {A} (l: list A): list (A * list A) := match l with | nil => nil | x :: xs => (x, xs) :: map (fun pq => (fst pq, x :: snd pq)) (separates xs) end.
imports: CoRN.algebra.RSetoid Unicode.Utf8 Setoid List Permutation Setoid Morphisms SetoidPermutation stdlib_omissions.Pair