proposition: Lemma map_lookup_imap {A B} (f : K → A → option B) (m : M A) i : map_imap f m !! i = m !! i ≫= f i.
proof: Proof. unfold map_imap; destruct (m !! i ≫= f i) as [y|] eqn:Hi; simpl. - destruct (m !! i) as [x|] eqn:?; simplify_eq/=. apply elem_of_list_to_map_1'. { intros y'; rewrite elem_of_list_omap; intros ([i' x']&Hi'&?). by rewrite elem_of_map_to_list in Hi'; simplify_option_eq. } apply elem_of_list_omap; exists (i,x); split; [by apply elem_of_map_to_list|by simplify_option_eq]. - apply not_elem_of_list_to_map; rewrite elem_of_list_fmap. intros ([i' x]&->&Hi'); simplify_eq/=. rewrite elem_of_list_omap in Hi'; destruct Hi' as ([j y]&Hj&?). rewrite elem_of_map_to_list in Hj; simplify_option_eq. Qed.
imports: Coq(Permutation) stdpp(options)