proposition: Lemma map_intersection_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (f : A → A → option A) (m1 m2a m2b : M A) : Proper ((≡) ==> (≡) ==> (≡)) f → (∀ y x1 x2, Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) → m1 ≡ intersection_with f m2a m2b ↔ ∃ m2a' m2b', m1 = intersection_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
proof: Proof. intros ? Hf. apply (merge_equiv_eq _ _ _ _ _). intros ? [x1|] [x2|]; simpl; first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq]; by repeat econstructor. Qed.
imports: Coq(Permutation) stdpp(options)