proposition: Theorem list_permut_trans : forall l1 l2 l3 : list elt, list_permut l1 l2 -> list_permut l2 l3 -> list_permut l1 l3.
proof: Proof. unfold list_permut, meq; intros; apply trans_eq with (multiplicity (list_to_multiset l2) a); trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid