proposition: Lemma permutation_Permutation : forall l l', Permutation l l' <-> permutation l l'.
proof: Proof. split. - induction 1. + apply permut_refl. + apply permut_cons; auto. + change (permutation (y::x::l) ((x::nil)++y::l)). apply permut_add_cons_inside; simpl; apply permut_refl. + apply permut_trans with l'; auto. - revert l'. induction l. + intros. rewrite (permut_nil (permut_sym H)). apply Permutation_refl. + intros. destruct (In_split _ _ (permut_cons_In H)) as (h2,(t2,H1)). subst l'. apply Permutation_cons_app. apply IHl. apply permut_remove_hd with a; auto with typeclass_instances. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation