proposition: Lemma map_fmap_equiv_eq `{Equiv A, !Equivalence (≡@{A}), Equiv B, !Equivalence (≡@{B})} (f : A → B) (m1 : M B) (m2 : M A) : Proper ((≡) ==> (≡)) f → (∀ y x, y ≡ f x → ∃ x', y = f x' ∧ x' ≡ x) → m1 ≡ f <$> m2 ↔ ∃ m2', m1 = f <$> m2' ∧ m2' ≡ m2.
proof: Proof. intros ? Hf. rewrite map_fmap_alt; setoid_rewrite map_fmap_alt. apply map_omap_equiv_eq; [solve_proper|]. intros ?? (?&->&?)%(inj _)%Hf; eauto. Qed.
imports: Coq(Permutation) stdpp(options)