proposition: Lemma Permutation_map_inv : forall l1 l2, Permutation l1 (map f l2) -> exists l3, l1 = map f l3 /\ Permutation l2 l3.
proof: Proof. induction l1; intros l2 HP. - exists nil; split; auto. apply Permutation_nil in HP. destruct l2; auto. inversion HP. - symmetry in HP. destruct (Permutation_vs_cons_inv HP) as [l3 [l4 Heq]]. destruct (map_eq_app _ _ _ _ Heq) as [l1' [l2' [Heq1 [Heq2 Heq3]]]]; subst. destruct (map_eq_cons _ _ Heq3) as [b [l1'' [Heq1' [Heq2' Heq3']]]]; subst. rewrite map_app in HP; simpl in HP. symmetry in HP. apply Permutation_cons_app_inv in HP. rewrite <- map_app in HP. destruct (IHl1 _ HP) as [l3 [Heq1'' Heq2'']]; subst. exists (b :: l3); split; auto. symmetry in Heq2''; symmetry; apply (Permutation_cons_app _ _ _ Heq2''). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat