proposition: Lemma map_omap_equiv_eq `{Equiv A, !Equivalence (≡@{A}), Equiv B, !Equivalence (≡@{B})} (f : A → option B) (m1 : M B) (m2 : M A) : Proper ((≡) ==> (≡)) f → (∀ y x, Some y ≡ f x → ∃ x', Some y = f x' ∧ x' ≡ x) → m1 ≡ omap f m2 ↔ ∃ m2', m1 = omap f m2' ∧ m2' ≡ m2.
proof: Proof. intros ? Hf. split; [|by intros (?&->&->)]. revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm. { rewrite omap_empty, map_empty_equiv_eq in Hm. subst m1. exists ∅. by rewrite omap_empty. } rewrite omap_insert in Hm. destruct (f x) as [y|] eqn:Hfx. - apply insert_equiv_eq in Hm as (y'&m1'&->&Hy&(m2'&->&?)%IH). destruct (Hf y' x) as (x'&Hfx'&?). { by rewrite Hfx, Hy. } exists (<[i:=x']> m2'). split; [|by f_equiv]. by rewrite omap_insert, <-Hfx'. - apply delete_equiv_eq in Hm as (m1'&->&(m2'&->&?)%IH). exists (<[i:=x]> m2'). split; [|by f_equiv]. by rewrite omap_insert, Hfx. Qed.
imports: Coq(Permutation) stdpp(options)