proposition: Lemma elem_of_list_bind (x : B) (l : list A) : x ∈ l ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ l.
proof: Proof. split. - induction l as [|y l IH]; csimpl; [inv 1|]. rewrite elem_of_app. intros [?|?]. + exists y. split; [done | by left]. + destruct IH as [z [??]]; [done|]. exists z. split; [done | by right]. - intros [y [Hx Hy]]. induction Hy; csimpl; rewrite elem_of_app; intuition. Qed.
imports: stdpp(options)