proposition: Lemma CPermutation_map_inv A B : forall (f : A -> B) m l, CPermutation m (map f l) -> exists l', m = map f l' /\ CPermutation l l'.
proof: Proof. induction m as [| b m]; intros l HC. - exists nil; split; auto. destruct l; auto. apply CPermutation_nil in HC; inversion HC. - symmetry in HC. destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]]. apply map_eq_app in Heq as [l1 [l1' [-> [<- Heq]]]]. apply map_eq_cons in Heq as [a [l1'' [-> [<- <-]]]]. exists (a :: l1'' ++ l1); split. + now simpl; rewrite map_app. + now rewrite app_comm_cons. Qed.
imports: List Permutation Morphisms PeanoNat