proposition: Lemma list_remove_Some_inv l k x : l ≡ₚ x :: k → ∃ k', list_remove x l = Some k' ∧ k ≡ₚ k'.
proof: Proof. intros. destruct (list_remove_Permutation (x :: k) l k x) as (k'&?&?). - done. - simpl; by case_decide. - by exists k'. Qed.
imports: stdpp(options)