proposition: Theorem list_permut_sym : forall l1 l2 : list elt, list_permut l1 l2 -> list_permut l2 l1.
proof: Proof. unfold list_permut, meq; intros; apply sym_eq; trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid