proposition: Lemma separates_elem_lengths {A} (l x: list A): In x (map (@snd _ _) (separates l)) → length l = S (length x).
proof: Proof. Proof with auto. revert x. induction l; simpl. intuition. intros x [[] | C]... rewrite map_map in C. simpl in C. destruct (proj1 (in_map_iff _ _ _) C) as [x0 [[]?]]. rewrite (IHl (snd x0)). reflexivity. apply in_map_iff. eauto. Qed.
imports: CoRN.algebra.RSetoid Unicode.Utf8 Setoid List Permutation Setoid Morphisms SetoidPermutation stdlib_omissions.Pair