proposition: Lemma CPermutation_image A B : forall (f : A -> B) a l l', CPermutation (a :: l) (map f l') -> exists a', a = f a'.
proof: Proof. intros f a l l' HP. now apply CPermutation_Permutation, Permutation_image in HP. Qed.
imports: List Permutation Morphisms PeanoNat