proposition: Lemma permut_app : forall l l' m m':list A, permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
proof: Proof. unfold permutation; intros. apply meq_trans with (munion (list_contents l) (list_contents m)); auto using permut_cons, list_contents_app with datatypes. apply meq_trans with (munion (list_contents l') (list_contents m')); auto using permut_cons, list_contents_app with datatypes. apply meq_trans with (munion (list_contents l') (list_contents m)); auto using permut_cons, list_contents_app with datatypes. Qed.
imports: Lia Relations Multiset SetoidList