proposition: Lemma list_find_elem_of l x : x ∈ l → P x → is_Some (list_find P l).
proof: Proof. induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto. by destruct IH as [[i x'] ->]; [|exists (S i, x')]. Qed.
imports: stdpp(options)