proposition: Lemma Permutation_pull_to_front {T} (a : T) ls (H : List.In a ls) : exists ls' : _, Permutation ls (a::ls').
proof: Proof. induction ls; simpl in *; destruct_head False. destruct_head_hnf or; subst. { exists ls; reflexivity. } { specialize (IHls H). destruct IHls as [ls' H']. eexists (_::ls'). etransitivity; [ apply perm_skip; exact H' | ]. apply perm_swap. } Qed.
imports: Coq.Lists.List Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common Fiat.Common.List.PermutationFacts