proposition: Lemma map_difference_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) : m1 ≡ m2a ∖ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∖ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
proof: Proof. apply map_difference_with_equiv_eq; [constructor|]. intros ??? [=]%None_equiv_eq. Qed.
imports: Coq(Permutation) stdpp(options)