proposition: Lemma PermutationConsSplit {A} : forall (a : A) (l l' : list A), Permutation (a :: l) l' -> exists l1' l2', l' = app l1' (a :: l2').
proof: Proof. intros. apply (Permutation_in a) in H; simpl; eauto. apply in_split; apply H; constructor; eauto. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts Coq.Program.Program Coq.Lists.SetoidList