proposition: Lemma elem_of_list_omap l y : y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
proof: Proof. split. - induction l as [|x l]; csimpl; repeat case_match; repeat (setoid_rewrite elem_of_nil || setoid_rewrite elem_of_cons); naive_solver. - intros (x&Hx&?). by induction Hx; csimpl; repeat case_match; simplify_eq; try constructor; auto. Qed.
imports: stdpp(options)