proposition: Theorem permutation_flat_map : forall (A B : Set) (f : A -> list B) l1 l2, Permutation l1 l2 -> Permutation (flat_map f l1) (flat_map f l2).
proof: Proof. intros A B f l1 l2 H; elim H; simpl in |- *; auto. intros a b l; auto. repeat rewrite <- app_ass. apply Permutation_app; auto. intros k3 l4 l5 H0 H1 H2 H3; apply perm_trans with (1 := H1); auto. Qed.
imports: List ListAux