proposition: Lemma list_permut_nil : forall l, list_permut l nil -> l = nil.
proof: Proof. intro l; destruct l as [ | e l ]; trivial. intros Abs; absurd (list_permut (e :: l) nil); trivial. unfold not; unfold list_permut, meq; intro H; generalize (H e); simpl; elim (eq_elt_dec e e). intros _; discriminate. intro; absurd (e=e); trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid