proposition: Lemma SetoidPermutation_meaning {A} (R: relation A) `{!Equivalence R} (x y: list A): SetoidPermutation R x y ↔ ∃ y', list_eq R x y' ∧ Permutation y y'.
proof: Proof. Proof with auto. split. intro H. induction H. exists nil. intuition. destruct IHSetoidPermutation as [?[??]]. exists (y :: x0). repeat split... exists (y :: x :: l). split... reflexivity. destruct IHSetoidPermutation1 as [x [H1 H3]]. destruct IHSetoidPermutation2 as [x0 [H2 H4]]. symmetry in H3. destruct (Perm_list_eq_commute R x l' x0 H3 H2). exists x1. split. transitivity x; intuition. transitivity x0; intuition. intros [?[E?]]. rewrite E. symmetry. apply SetoidPermutation_from_Permutation... apply _. Qed.
imports: Coq.Unicode.Utf8 Coq.Setoids.Setoid CoRN.stdlib_omissions.List Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms