proposition: Lemma elem_of_lookup_imap_1 l x : x ∈ imap f l → ∃ i y, x = f i y ∧ l !! i = Some y.
proof: Proof. intros [i Hin]%elem_of_list_lookup. rewrite list_lookup_imap in Hin. simplify_option_eq; naive_solver. Qed.
imports: stdpp(options)