proposition: Lemma permutation_cons_in : forall {A} {s1 s2 item}, Permutation (s1) (item :: s2) -> @List.In A item s1.
proof: Proof. intros. eapply Permutation_in; try symmetry; eauto; intuition. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts