proposition: Lemma SetoidPermutation_eq {A} (a b: list A): SetoidPermutation eq a b ↔ Permutation a b.
proof: Proof. split; intro; induction H; eauto. subst; eauto. Qed.
imports: Coq.Unicode.Utf8 Coq.Setoids.Setoid CoRN.stdlib_omissions.List Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms