proposition: Theorem permutation_map : forall (A B : Set) (f : A -> B) l1 l2, permutation l1 l2 -> permutation (map f l1) (map f l2).
proof: Proof. intros A B f l1 l2 H; elim H; simpl in |- *; auto. intros l0 l3 l4 H0 H1 H2 H3; apply permutation_trans with (2 := H3); auto. Qed.
imports: List ListAux