proposition: Lemma move_to_front {A} (x: A) (l: list A): In x l → exists l', Permutation (x :: l') l.
proof: Proof. Proof with eauto. induction l; simpl. intuition. intros [[] | D]... destruct (IHl D) as [y ?]. exists (a :: y). rewrite perm_swap... Qed.
imports: Coq.Lists.List Coq.Unicode.Utf8 Coq.Setoids.Setoid Coq.Sorting.Permutation Coq.Setoids.Setoid Coq.Classes.Morphisms CoRN.stdlib_omissions.Pair