proposition: Lemma elem_of_list_split_l `{EqDecision A} l x : x ∈ l → ∃ l1 l2, l = l1 ++ x :: l2 ∧ x ∉ l1.
proof: Proof. induction 1 as [x l|x y l ? IH]. { exists [], l. rewrite elem_of_nil. naive_solver. } destruct (decide (x = y)) as [->|?]. - exists [], l. rewrite elem_of_nil. naive_solver. - destruct IH as (l1 & l2 & -> & ?). exists (y :: l1), l2. rewrite elem_of_cons. naive_solver. Qed.
imports: stdpp(options)