proposition: Lemma Permutation_elt_map_inv: forall l1 l2 l3 l4 a, Permutation (l1 ++ a :: l2) (l3 ++ map f l4) -> (forall b, a <> f b) -> exists l1' l2', l3 = l1' ++ a :: l2'.
proof: Proof. intros l1 l2 l3 l4 a HP Hf. apply (Permutation_in a), in_app_or in HP; [| now apply in_elt]. destruct HP as [HP%in_split | (x & Heq & ?)%in_map_iff]; trivial; subst. now contradiction (Hf x). Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat