proposition: Lemma permut_length_1: forall a b, permutation (a :: nil) (b :: nil) -> a=b.
proof: Proof. intros a b; unfold PermutSetoid.permutation, meq; intro P; generalize (P b); clear P; simpl. destruct (eq_dec b b) as [H|H]; [ | destruct H; auto]. destruct (eq_dec a b); simpl; auto; intros; discriminate. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation