proposition: Lemma permutation_cons: forall l l' a, permutation eqA_dec (a :: l) l' -> exists p a', nth_error l' p = Some a' /\ eqA a a' /\ permutation eqA_dec l (drop_nth l' p).
proof: Proof. intros. destruct (permutation_in a H) as [a' [aa' a'l']]. auto with datatypes. destruct (list_In_nth l' a' a'l') as [p l'p]. exists p; exists a'; split; [idtac | split]; trivial. intuition. apply permutation_drop with a a'; trivial. intuition. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)