proposition: Lemma elem_of_list_split_r `{EqDecision A} l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l2.
proof: Proof. induction l as [|y l IH] using rev_ind. { by rewrite elem_of_nil. } destruct (decide (x = y)) as [->|]. - exists l, []. rewrite elem_of_nil. naive_solver. - rewrite elem_of_app, elem_of_list_singleton. intros [?| ->]; try done. destruct IH as (l1 & l2 & -> & ?); auto. exists l1, (l2 ++ [y]). rewrite elem_of_app, elem_of_list_singleton, <-(assoc_L (++)). naive_solver. Qed.
imports: stdpp(options)