proposition: Lemma separates_length {A} (l: list A): length (separates l) = length l.
proof: Proof. induction l. intuition. simpl. rewrite map_length. congruence. Qed.
imports: CoRN.algebra.RSetoid Unicode.Utf8 Setoid List Permutation Setoid Morphisms SetoidPermutation stdlib_omissions.Pair