proposition: Lemma Permutation_image : forall a l l', Permutation (a :: l) (map f l') -> exists a', a = f a'.
proof: Proof. intros a l l' HP. destruct (Permutation_map_inv _ HP) as [l'' [Heq _]]. destruct l'' as [ | a' l'']; inversion_clear Heq. now exists a'. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat