proposition: Lemma list_remove_Some l k x : list_remove x l = Some k → l ≡ₚ x :: k.
proof: Proof. revert k. induction l as [|y l IH]; simpl; intros k ?; [done |]. simplify_option_eq; auto. by rewrite Permutation_swap, <-IH. Qed.
imports: stdpp(options)