proposition: Lemma delete_Permutation l i x : l !! i = Some x → l ≡ₚ x :: delete i l.
proof: Proof. revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto. by rewrite Permutation_swap, <-(IH i). Qed.
imports: stdpp(options)