diff --git a/Util/MMultiset/MMultisetExtraOps.v b/Util/MMultiset/MMultisetExtraOps.v
index df83277bc5452cb24281eb631e066c11b5237166..bd5ae5abcf3ca3e46bd0e71a82b9d5cbcf7881d3 100644
--- a/Util/MMultiset/MMultisetExtraOps.v
+++ b/Util/MMultiset/MMultisetExtraOps.v
@@ -225,14 +225,18 @@ Section MMultisetExtra.
 
   (** **  Function [map] and its properties  **)
 
-  Definition map f m := fold (fun x n acc => add (f x) n acc) m empty.
-
   Section map_results.
-    Variable f : elt -> elt.
+
+    Context {elt2 : Type}.
+    Context `{M2 : FMultisetsOn elt2}.
+
+    Definition map (f : elt -> elt2) m := fold (fun x n acc => add (f x) n acc) m empty.
+
+    Variable f : elt -> elt2.
     Hypothesis Hf : Proper (equiv ==> equiv) f.
 
     Global Instance map_compat : Proper (equiv ==> equiv) (map f).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros m₁ m₂ Hm. unfold map. apply (fold_compat _ _).
     - repeat intro. msetdec.
     - repeat intro. apply add_comm.
@@ -241,22 +245,23 @@ Section MMultisetExtra.
     Qed.
 
     Lemma map_In : forall x m, In x (map f m) <-> exists y, x == (f y) /\ In y m.
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros x m. unfold In, map. apply fold_rect.
-    + intros m₁ m₂ acc Heq Hequiv. rewrite Hequiv. now setoid_rewrite Heq.
-    + setoid_rewrite empty_spec. split; try intros [? [_ ?]]; lia.
-    + intros y m' acc Hm Hin Hrec. destruct (equiv_dec x (f y)) as [Heq | Hneq]; msetdec.
-      - split.
-          intros. exists y. split; trivial. msetdec.
-          intros [? [? ?]]. msetdec.
-      - rewrite Hrec. split; intros [z [Heq ?]]; exists z; split; msetdec.
+    * intros m₁ m₂ acc Heq Hequiv. rewrite Hequiv. now setoid_rewrite Heq.
+    * setoid_rewrite empty_spec. split; try intros [? [_ ?]]; lia.
+    * intros y m' acc Hm Hin Hrec. destruct (equiv_dec x (f y)) as [Heq | Hneq]. (* ; msetdec. *)
+      + split.
+        - intros. exists y. split; trivial. msetdec.
+        - intros [? [? ?]]. rewrite <- Heq, add_same.
+          destruct (equiv_dec y x0) as [Heq' | Hneq']; msetdec.
+      + msetdec. rewrite Hrec. split; intros [z [Heq ?]]; exists z; split; msetdec.
     Qed.
 
     Lemma map_empty : map f empty == empty.
     Proof using M f. unfold map. now rewrite fold_empty. Qed.
 
     Lemma map_add : forall x n m, map f (add x n m) == add (f x) n (map f m).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros x n m y. destruct n.
     + now do 2 rewrite add_0.
     + unfold map at 1. rewrite (fold_add_additive _).
@@ -269,50 +274,55 @@ Section MMultisetExtra.
 
     Lemma map_spec : forall x m,
       (map f m)[x] = cardinal (nfilter (fun y _ => if equiv_dec (f y) x then true else false) m).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros x m. pose (g := fun y (_ : nat) => if equiv_dec (f y) x then true else false). fold g.
     assert (Hg : Proper (equiv ==> @Logic.eq nat ==> Logic.eq) g). { repeat intro. unfold g. msetdec. }
     pattern m. apply ind; clear m.
     + intros ? ? Hm. now rewrite Hm.
-    + intros * Hin Hrec. rewrite map_add, nfilter_add; trivial. unfold g at 2. msetdec. rewrite cardinal_add. lia.
+    + intros * Hin Hrec. rewrite map_add, nfilter_add; trivial. unfold g at 2.
+      destruct (equiv_dec (f x0) x) as [Heq | Hneq].
+      - rewrite Heq, cardinal_add, add_same. lia.
+      - msetdec.
     + now rewrite map_empty, nfilter_empty, cardinal_empty, empty_spec.
     Qed.
 
     Global Instance map_sub_compat : Proper (Subset ==> Subset) (map f).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intro m. pattern m. apply ind; clear m.
     + intros ? ? Hm. now setoid_rewrite Hm.
     + intros m x n Hin Hn Hrec m' Hsub y.
       assert (Hx : m[x] = 0). { unfold In in Hin. lia. }
-      rewrite <- (add_remove_cancel x m' (Hsub x)). do 2 rewrite (map_add _). msetdec.
-      - apply Nat.add_le_mono; trivial; [].
-        repeat rewrite map_spec; trivial. apply add_subset_remove in Hsub.
-        apply cardinal_sub_compat, nfilter_sub_compat; solve [lia | repeat intro; msetdec].
-      - now apply Hrec, add_subset_remove.
+      rewrite <- (add_remove_cancel x m' (Hsub x)). do 2 rewrite (map_add _).
+      apply add_sub_compat.
+      - reflexivity.
+      - msetdec.
+      - apply Hrec, add_subset_remove. msetdec.
     + intros ? _. rewrite map_empty. apply subset_empty_l.
     Qed.
 
     Lemma map_singleton : forall x n, map f (singleton x n) == singleton (f x) n.
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros x n y. destruct n.
     + repeat rewrite singleton_0. now rewrite map_empty. 
-    + unfold map. rewrite fold_singleton; repeat intro; msetdec.
+    + unfold map. rewrite fold_singleton; repeat intro; try lia.
+      - apply add_empty.
+      - msetdec.
     Qed.
 
     Lemma map_remove1 : forall x n m, n <= m[x] -> map f (remove x n m) == remove (f x) n (map f m).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros x n m Hle. rewrite <- (add_remove_cancel _ _ Hle) at 2. now rewrite (map_add _), remove_add_cancel.
     Qed.
 
     Lemma map_remove2 : forall x n m,
       m[x] <= n -> map f (remove x n m) == remove (f x) m[x] (map f m).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros x n m Hle. rewrite <- (add_remove_id _ _ Hle) at 3.
     now rewrite (map_add _), remove_add_cancel.
     Qed.
 
     Lemma fold_map_union : forall m₁ m₂, fold (fun x n acc => add (f x) n acc) m₁ m₂ == union (map f m₁) m₂.
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros m₁ m₂. apply fold_rect with (m := m₁).
     + repeat intro. msetdec.
     + now rewrite map_empty, union_empty_l.
@@ -320,7 +330,7 @@ Section MMultisetExtra.
     Qed.
 
     Theorem map_union : forall m₁ m₂, map f (union m₁ m₂) == union (map f m₁) (map f m₂).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros m₁ m₂. unfold map at 1 2. rewrite (fold_union_additive _).
     + now apply fold_map_union.
     + repeat intro. msetdec.
@@ -329,7 +339,7 @@ Section MMultisetExtra.
     Qed.
 
     Theorem map_inter : forall m₁ m₂, map f (inter m₁ m₂) [<=] inter (map f m₁) (map f m₂).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros m1 m2 x. destruct (map f (inter m1 m2))[x] eqn:Hfx.
     + lia.
     + assert (Hin : In x (map f (inter m1 m2))) by msetdec.
@@ -339,7 +349,7 @@ Section MMultisetExtra.
     Qed.
 
     Theorem map_lub : forall m₁ m₂, lub (map f m₁) (map f m₂) [<=] map f (lub m₁ m₂).
-    Proof using Hf M.
+    Proof using Hf M M2.
     intros m1 m2 x. destruct (lub (map f m1) (map f m2))[x] eqn:Hfx.
     + lia.
     + assert (Hin : In x (lub (map f m1) (map f m2))).
@@ -353,14 +363,14 @@ Section MMultisetExtra.
     
     Lemma map_from_elements :
       forall l, map f (from_elements l) == from_elements (List.map (fun xn => (f (fst xn), snd xn)) l).
-    Proof using Hf M.
+    Proof using Hf M M2.
     induction l as [| [x n] l].
     - apply map_empty.
     - simpl from_elements. rewrite map_add. f_equiv. apply IHl.
     Qed.
-    
+
     Lemma map_support : forall m, inclA equiv (support (map f m)) (List.map f (support m)).
-    Proof using Hf M.
+    Proof using Hf M M2.
     apply ind.
     * repeat intro. msetdec.
     * intros m x n Hin Hn Hrec. rewrite map_add; trivial. repeat rewrite support_add; try lia.
@@ -371,17 +381,17 @@ Section MMultisetExtra.
         - right. now apply Hrec.
     * now rewrite map_empty, support_empty.
     Qed.
-    
+
     Lemma map_cardinal : forall m, cardinal (map f m) = cardinal m.
-    Proof using Hf M.
+    Proof using Hf M M2.
     apply ind.
     + repeat intro. msetdec.
     + intros m x n Hin Hn Hrec. rewrite (map_add _). do 2 rewrite cardinal_add. now rewrite Hrec.
-    + now rewrite map_empty.
+    + now rewrite map_empty, 2 cardinal_empty.
     Qed.
-    
+
     Lemma map_size : forall m, size (map f m) <= size m.
-    Proof using Hf M.
+    Proof using Hf M M2.
     apply ind.
     + repeat intro. msetdec.
     + intros m x n Hm Hn Hrec. rewrite map_add, size_add, size_add; trivial.
@@ -390,69 +400,71 @@ Section MMultisetExtra.
       - contradiction Hinf. rewrite map_In. now exists x.
       - lia.
       - lia.
-    + now rewrite map_empty.
+    + now rewrite map_empty, 2 size_empty.
     Qed.
-    
+
     Section map_injective_results.
       Hypothesis Hf2 : injective equiv equiv f.
-      
+
       Lemma map_injective_spec : forall x m, (map f m)[f x] = m[x].
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros x m. unfold map. apply fold_rect.
       + repeat intro. msetdec.
       + now do 2 rewrite empty_spec.
       + intros y m' acc Hin Hm Heq. destruct (equiv_dec x y) as [Hxy | Hxy].
-        - msetdec.
+        - rewrite <- Hxy, 2 add_same. lia.
         - repeat rewrite add_other; trivial. intro Habs. apply Hxy. now apply Hf2.
       Qed.
-      
+
       Corollary map_injective_In : forall x m, In (f x) (map f m) <-> In x m.
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros x m. rewrite map_In; trivial. split; intro Hin.
       + destruct Hin as [y [Heq Hin]]. apply Hf2 in Heq. now rewrite Heq.
       + now exists x.
       Qed.
-      
+
       Lemma map_injective_remove : forall x n m, map f (remove x n m) == remove (f x) n (map f m).
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros x n m. destruct (Compare_dec.le_dec n m[x]) as [Hle | Hlt].
       * now apply map_remove1.
-      * intro y. msetdec.
-        + repeat rewrite map_injective_spec; trivial. msetdec.
+      * intro y. destruct (equiv_dec y (f x)) as [Heq | Hneq].
+        + now rewrite Heq, map_injective_spec, 2 remove_same, map_injective_spec.
         + destruct (In_dec y (map f m)) as [Hin | Hin].
           - rewrite (map_In _) in Hin. destruct Hin as [z [Heq Hz]]. msetdec.
             repeat rewrite map_injective_spec; trivial. msetdec.
-          - rewrite not_In in Hin. rewrite Hin, <- not_In, (map_In _).
+          - rewrite not_In in Hin. msetdec. rewrite <- not_In, (map_In _).
             intros [z [Heq Hz]]. msetdec. rewrite map_injective_spec in Hin; trivial. lia.
       Qed.
-      
+
       Theorem map_injective_inter : forall m₁ m₂, map f (inter m₁ m₂) == inter (map f m₁) (map f m₂).
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros m₁ m₂ x. destruct ((inter (map f m₁) (map f m₂))[x]) eqn:Hn.
       + rewrite <- not_In in Hn |- *. intro Habs. apply Hn.
-        rewrite (map_In _) in Habs. destruct Habs as [y [Heq Hy]]. msetdec.
-        unfold gt in *. rewrite Nat.min_glb_lt_iff in *. now repeat rewrite map_injective_spec.
+        rewrite (map_In _) in Habs. destruct Habs as [y [Heq Hy]].
+        unfold In, gt in *. rewrite 2 inter_spec in *.
+        now rewrite Heq, 2 map_injective_spec.
       + rewrite inter_spec in Hn.
         assert (Hx : In x (map f m₁)).
         { msetdec. }
         rewrite map_In in *; trivial. destruct Hx as [y [Heq Hy]]. msetdec.
         do 2 (rewrite map_injective_spec in *; trivial). msetdec.
       Qed.
-      
+
       Theorem map_injective_diff : forall m₁ m₂, map f (diff m₁ m₂) == diff (map f m₁) (map f m₂).
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros m₁ m₂ x. destruct ((diff (map f m₁) (map f m₂))[x]) eqn:Hn.
       + rewrite <- not_In in Hn |- *. intro Habs. apply Hn.
         rewrite (map_In _) in Habs. destruct Habs as [y [Heq Hy]]. msetdec.
-        now repeat rewrite map_injective_spec.
-      + assert (Hx : In x (map f m₁)) by msetdec.
+        now rewrite diff_spec, 2 map_injective_spec.
+      + rewrite diff_spec in *.
+        assert (Hx : In x (map f m₁)) by msetdec.
         rewrite map_In in *; trivial. destruct Hx as [y [Heq _]]. msetdec.
         do 2 (rewrite map_injective_spec in *; trivial). msetdec.
       Qed.
-      
+
       Lemma map_injective_lub_wlog : forall x m₁ m₂, (map f m₂)[x] <= (map f m₁)[x] ->
         (map f (lub m₁ m₂))[x] = (map f m₁)[x].
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros x m₁ m₂ Hle. destruct (map f m₁)[x] eqn:Heq1.
       - apply Nat.le_0_r in Hle. destruct (map f (lub m₁ m₂))[x] eqn:Heq2; trivial.
         assert (Hin : In x (map f (lub m₁ m₂))). { unfold In. lia. }
@@ -462,38 +474,38 @@ Section MMultisetExtra.
         rewrite map_In in Hin. destruct Hin as [y [Heq Hin]]. rewrite Heq, map_injective_spec in *.
         rewrite lub_spec. rewrite Nat.max_l; lia.
       Qed.
-      
+
       Theorem map_injective_lub : forall m₁ m₂, map f (lub m₁ m₂) == lub (map f m₁) (map f m₂).
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros m₁ m₂ x. rewrite lub_spec. apply Nat.max_case_strong; intro Hle.
       - now apply map_injective_lub_wlog.
       - rewrite lub_comm. now apply map_injective_lub_wlog.
       Qed.
-      
+
       Lemma map_injective : injective equiv equiv (map f).
-      Proof using Hf Hf2 M. intros ? ? Hm x. specialize (Hm (f x)). repeat (rewrite map_injective_spec in Hm; trivial). Qed.
-      
+      Proof using Hf Hf2 M M2. intros ? ? Hm x. specialize (Hm (f x)). repeat (rewrite map_injective_spec in Hm; trivial). Qed.
+
       Lemma map_injective_subset : forall m₁ m₂, map f m₁ [<=] map f m₂ <-> m₁ [<=] m₂.
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       intros m₁ m₂. split; intro Hincl.
       - intro x. setoid_rewrite <- map_injective_spec. apply Hincl.
       - now apply map_sub_compat.
       Qed.
-      
+
       Lemma map_injective_elements : forall m,
         PermutationA eq_pair (elements (map f m)) (List.map (fun xn => (f (fst xn), snd xn)) (elements m)).
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       assert (Proper (eq_pair ==> eq_pair) (fun xn => (f (fst xn), snd xn))). { intros ? ? Heq. now rewrite Heq. }
       apply ind.
       + repeat intro. msetdec.
       + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite elements_add_out; trivial.
         - simpl. now constructor.
         - rewrite (map_In _). intros [y [Heq Hy]]. apply Hf2 in Heq. apply Hin. now rewrite Heq.
-      + now rewrite map_empty, elements_empty.
+      + now rewrite map_empty, 2 elements_empty.
       Qed.
-      
+
       Lemma map_injective_support : forall m, PermutationA equiv (support (map f m)) (List.map f (support m)).
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       apply ind.
       * repeat intro. msetdec.
       * intros m x n Hin Hrec. rewrite map_add; trivial. repeat rewrite support_add; try lia.
@@ -503,11 +515,11 @@ Section MMultisetExtra.
           - rewrite support_spec in Habs. unfold In in *. contradiction.
           - simpl. destruct (In_dec x m); try contradiction. rewrite <- map_injective_In in Hin; trivial.
             destruct (In_dec (f x) (map f m)); try contradiction. now apply PermutationA_cons.
-      * now rewrite map_empty, support_empty.
+      * now rewrite map_empty, 2 support_empty.
       Qed.
-      
+
       Lemma map_injective_size : forall m, size (map f m) = size m.
-      Proof using Hf Hf2 M.
+      Proof using Hf Hf2 M M2.
       apply ind.
       + repeat intro. msetdec.
       + intros m x n Hin Hn Hrec. rewrite (map_add _). rewrite size_add, Hrec; trivial.
@@ -515,133 +527,129 @@ Section MMultisetExtra.
         - rewrite map_In in Hinf; trivial. destruct Hinf as [y [Heq Hiny]].
           apply Hf2 in Heq. rewrite Heq in Hin. contradiction.
         - rewrite size_add; trivial. destruct (In_dec x m); reflexivity || contradiction.
-      + now rewrite map_empty.
+      + now rewrite map_empty, 2 size_empty.
       Qed.
-      
+
     End map_injective_results.
   End map_results.
-  
-  Lemma map_extensionality_compat : forall f g, Proper (equiv ==> equiv) f ->
-    (forall x, equiv (g x) (f x)) -> forall m, map g m == map f m.
-  Proof using M.
-  intros f g Hf Hext m x.
-  assert (Hg : Proper (equiv ==> equiv) g). { intros ? ? Heq. do 2 rewrite Hext. now apply Hf. }
-  repeat rewrite map_spec; trivial. f_equiv. apply nfilter_extensionality_compat.
-  - intros y z Heq _ _ _. destruct (equiv_dec (g y) x), (equiv_dec (g z) x); trivial; rewrite Heq in *; contradiction.
-  - intros y _. destruct (equiv_dec (f y) x), (equiv_dec (g y) x); trivial; rewrite Hext in *; contradiction.
-  Qed.
-  
-  Lemma map_extensionality_compat_strong : forall f g, Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
-    forall m, (forall x, In x m -> equiv (g x) (f x)) -> map g m == map f m.
-  Proof using M.
-  intros f g Hf Hg m Hext x.
-  repeat rewrite map_spec; trivial. f_equiv. apply nfilter_extensionality_compat_strong.
-  - intros y z Heq _ _ _. destruct (equiv_dec (g y) x), (equiv_dec (g z) x); trivial; rewrite Heq in *; contradiction.
-  - intros y z Heq _ _ _. destruct (equiv_dec (f y) x), (equiv_dec (f z) x); trivial; rewrite Heq in *; contradiction.
-  - intros y Hin. destruct (equiv_dec (f y) x), (equiv_dec (g y) x); rewrite Hext in *; trivial; contradiction.
-  Qed.
-  
-  Lemma map_merge : forall f g, Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
-    forall m, map f (map g m) == map (fun x => f (g x)) m.
-  Proof using M.
-  intros f g Hf Hg.
-  apply ind.
-  + repeat intro. msetdec.
-  + intros m x n Hin Hn Hrec. repeat rewrite map_add; refine _. now rewrite Hrec.
-  + now repeat rewrite map_empty.
-  Qed.
-  
-  Lemma map_id : forall m, map id m == m.
-  Proof using M.
-  intro m. intro x. change x with (id x) at 1.
-  rewrite map_injective_spec; autoclass; []. now repeat intro.
-  Qed.
-  
-  Theorem map_injective_fold : forall A eqA, Equivalence eqA ->
-    forall f g, Proper (equiv ==> Logic.eq ==> eqA ==> eqA) f -> transpose2 eqA f ->
-    Proper (equiv ==> equiv) g -> injective equiv equiv g ->
-    forall m (i : A), eqA (fold f (map g m) i) (fold (fun x => f (g x)) m i).
-  Proof using M.
-  intros A eqA HeqA f g Hf Hf2 Hg Hg2 m.
-  assert (Hfg2 : transpose2 eqA (fun x => f (g x))). { repeat intro. apply Hf2. }
-  pattern m. apply ind.
-  + intros m₁ m₂ Hm. split; intros Heq i; rewrite fold_compat; trivial;
-    solve [rewrite Heq; now apply fold_compat; refine _ | now rewrite Hm | reflexivity].
-  + intros m' x n Hin Hn Hrec i. rewrite fold_compat; try apply map_add; reflexivity || trivial.
-    repeat rewrite fold_add; trivial; refine _.
-    - now rewrite Hrec.
-    - rewrite (map_In _). intros [y [Heq Hy]]. apply Hin. apply Hg2 in Heq. now rewrite Heq.
-  + intro. rewrite fold_compat; apply map_empty || reflexivity || trivial. now do 2 rewrite fold_empty.
-  Qed.
-  
-  Lemma map_injective_nfilter : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
-    forall m, nfilter f (map g m) == map g (nfilter (fun x => f (g x)) m).
-  Proof using M.
-  intros f g Hf Hg Hg2. apply ind.
-  + repeat intro. msetdec.
-  + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite nfilter_add; trivial.
-    - destruct (f (g x) n).
-        now rewrite map_add, Hrec.
-        apply Hrec.
-    - refine _. 
-    - rewrite (map_In _). intros [y [Heq Hy]]. apply Hg2 in Heq. apply Hin. now rewrite Heq.
-  + rewrite map_empty. now rewrite nfilter_empty, nfilter_empty, map_empty; autoclass.
-  Qed.
-  
-  Lemma map_injective_npartition_fst : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
-    forall m, fst (npartition f (map g m)) == map g (fst (npartition (fun x => f (g x)) m)).
-  Proof using M. intros. repeat rewrite npartition_spec_fst; refine _. now apply map_injective_nfilter. Qed.
-  
-  Lemma map_injective_npartition_snd : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
-    forall m, snd (npartition f (map g m)) == map g (snd (npartition (fun x => f (g x)) m)).
-  Proof using M.
-  intros. repeat rewrite npartition_spec_snd; refine _. apply map_injective_nfilter; trivial. repeat intro. msetdec.
-  Qed.
-  
-  Lemma map_injective_for_all : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
-    forall m, for_all f (map g m) = for_all (fun x => f (g x)) m.
-  Proof using M.
-  intros f g Hf Hg Hg2. apply ind.
-  + repeat intro. msetdec.
-  + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite for_all_add; trivial.
-    - now rewrite Hrec.
-    - refine _.
-    - now rewrite map_injective_In.
-  + rewrite map_empty. repeat rewrite for_all_empty; autoclass.
-  Qed.
-  
-  Lemma map_injective_exists : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
-    forall m, exists_ f (map g m) = exists_ (fun x => f (g x)) m.
-  Proof using M.
-  intros f g Hf Hg Hg2. apply ind.
-  + repeat intro. msetdec.
-  + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite exists_add; trivial.
-    - now rewrite Hrec.
-    - refine _. 
-    - rewrite (map_In _). intros [y [Heq Hy]]. apply Hg2 in Heq. apply Hin. now rewrite Heq.
-  + rewrite map_empty. repeat rewrite exists_empty; autoclass.
-  Qed.
-  
-  Theorem map_filter : forall f g, Proper (equiv ==> Logic.eq) f -> Proper (equiv ==> equiv) g ->
-    forall m, filter f (map g m) == map g (filter (fun x => f (g x)) m).
-  Proof using M.
-  intros f g Hf Hg. apply ind.
-  + intros m1 m2 Hm. now rewrite Hm.
-  + intros m x n Hin Hn Hrec. rewrite map_add, 2 filter_add; autoclass; [].
-    destruct (f (g x)).
-    - rewrite map_add; trivial; []. f_equiv. apply Hrec.
-    - apply Hrec.
-  + rewrite map_empty, 2 filter_empty, map_empty; autoclass; reflexivity.
-  Qed.
-  
-  Lemma map_partition_fst : forall f g, Proper (equiv ==> Logic.eq) f -> Proper (equiv ==> equiv) g ->
-    forall m, fst (partition f (map g m)) == map g (fst (partition (fun x => f (g x)) m)).
-  Proof using M. intros. rewrite 2 partition_spec_fst; try apply map_filter; autoclass. Qed.
-  
-  Lemma map_partition_snd : forall f g, Proper (equiv ==> Logic.eq) f -> Proper (equiv ==> equiv) g ->
-    forall m, snd (partition f (map g m)) == map g (snd (partition (fun x => f (g x)) m)).
-  Proof using M. intros. rewrite 2 partition_spec_snd; try apply map_filter; autoclass. Qed.
-  
+
+  Section map_extensionality_results.
+    Context {elt2 : Type}.
+    Context `{M2 : FMultisetsOn elt2}.
+
+    Lemma map_extensionality_compat : forall f g : elt -> elt2, Proper (equiv ==> equiv) f ->
+      (forall x, equiv (g x) (f x)) -> forall m, map g m == map f m.
+    Proof using M M2.
+    intros f g Hf Hext m x.
+    assert (Hg : Proper (equiv ==> equiv) g). { intros ? ? Heq. do 2 rewrite Hext. now apply Hf. }
+    repeat rewrite map_spec; trivial. f_equiv. apply nfilter_extensionality_compat.
+    - intros y z Heq _ _ _. destruct (equiv_dec (g y) x), (equiv_dec (g z) x); trivial; rewrite Heq in *; contradiction.
+    - intros y _. destruct (equiv_dec (f y) x), (equiv_dec (g y) x); trivial; rewrite Hext in *; contradiction.
+    Qed.
+
+    Lemma map_extensionality_compat_strong : forall f g : elt -> elt2,
+      Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
+      forall m, (forall x, In x m -> equiv (g x) (f x)) -> map g m == map f m.
+    Proof using M M2.
+    intros f g Hf Hg m Hext x.
+    repeat rewrite map_spec; trivial. f_equiv. apply nfilter_extensionality_compat_strong.
+    - intros y z Heq _ _ _. destruct (equiv_dec (g y) x), (equiv_dec (g z) x); trivial; rewrite Heq in *; contradiction.
+    - intros y z Heq _ _ _. destruct (equiv_dec (f y) x), (equiv_dec (f z) x); trivial; rewrite Heq in *; contradiction.
+    - intros y Hin. destruct (equiv_dec (f y) x), (equiv_dec (g y) x); rewrite Hext in *; trivial; contradiction.
+    Qed.
+
+    Lemma map_id : forall m, map id m == m.
+    Proof using M.
+    intro m. intro x. change x with (id x) at 1.
+    rewrite map_injective_spec; autoclass; []. now repeat intro.
+    Qed.
+
+    Theorem map_injective_fold : forall A eqA, Equivalence eqA ->
+      forall f g, Proper (equiv ==> Logic.eq ==> eqA ==> eqA) f -> transpose2 eqA f ->
+      Proper (equiv ==> equiv) g -> injective equiv equiv g ->
+      forall m (i : A), eqA (fold f (map g m) i) (fold (fun x => f (g x)) m i).
+    Proof using M M2.
+    intros A eqA HeqA f g Hf Hf2 Hg Hg2 m.
+    assert (Hfg2 : transpose2 eqA (fun x => f (g x))). { repeat intro. apply Hf2. }
+    pattern m. apply ind.
+    + intros m₁ m₂ Hm. split; intros Heq i; rewrite fold_compat; trivial;
+      solve [rewrite Heq; now apply fold_compat; refine _ | now rewrite Hm | reflexivity].
+    + intros m' x n Hin Hn Hrec i. rewrite fold_compat; try apply map_add; reflexivity || trivial.
+      repeat rewrite fold_add; trivial; refine _.
+      - now rewrite Hrec.
+      - rewrite (map_In _). intros [y [Heq Hy]]. apply Hin. apply Hg2 in Heq. now rewrite Heq.
+    + intro. rewrite fold_compat; apply map_empty || reflexivity || trivial. now do 2 rewrite fold_empty.
+    Qed.
+
+    Lemma map_injective_nfilter : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
+      forall m, nfilter f (map g m) == map g (nfilter (fun x => f (g x)) m).
+    Proof using M M2.
+    intros f g Hf Hg Hg2. apply ind.
+    + repeat intro. msetdec.
+    + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite nfilter_add; trivial.
+      - destruct (f (g x) n).
+        -- now rewrite map_add, Hrec.
+        -- apply Hrec.
+      - refine _. 
+      - rewrite (map_In _). intros [y [Heq Hy]]. apply Hg2 in Heq. apply Hin. now rewrite Heq.
+    + rewrite map_empty. now rewrite nfilter_empty, nfilter_empty, map_empty; autoclass.
+    Qed.
+
+    Lemma map_injective_npartition_fst : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
+      forall m, fst (npartition f (map g m)) == map g (fst (npartition (fun x => f (g x)) m)).
+    Proof using M M2. intros. repeat rewrite npartition_spec_fst; refine _. now apply map_injective_nfilter. Qed.
+
+    Lemma map_injective_npartition_snd : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
+      forall m, snd (npartition f (map g m)) == map g (snd (npartition (fun x => f (g x)) m)).
+    Proof using M M2.
+    intros. repeat rewrite npartition_spec_snd; refine _. apply map_injective_nfilter; trivial. repeat intro. msetdec.
+    Qed.
+
+    Lemma map_injective_for_all : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
+      forall m, for_all f (map g m) = for_all (fun x => f (g x)) m.
+    Proof using M M2.
+    intros f g Hf Hg Hg2. apply ind.
+    + repeat intro. msetdec.
+    + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite for_all_add; trivial.
+      - now rewrite Hrec.
+      - refine _.
+      - now rewrite map_injective_In.
+    + rewrite map_empty. repeat rewrite for_all_empty; autoclass.
+    Qed.
+
+    Lemma map_injective_exists : forall f g, compatb f -> Proper (equiv ==> equiv) g -> injective equiv equiv g ->
+      forall m, exists_ f (map g m) = exists_ (fun x => f (g x)) m.
+    Proof using M M2.
+    intros f g Hf Hg Hg2. apply ind.
+    + repeat intro. msetdec.
+    + intros m x n Hin Hn Hrec. rewrite (map_add _). repeat rewrite exists_add; trivial.
+      - now rewrite Hrec.
+      - refine _. 
+      - rewrite (map_In _). intros [y [Heq Hy]]. apply Hg2 in Heq. apply Hin. now rewrite Heq.
+    + rewrite map_empty. repeat rewrite exists_empty; autoclass.
+    Qed.
+
+    Theorem map_filter : forall f g, Proper (equiv ==> Logic.eq) f -> Proper (equiv ==> equiv) g ->
+      forall m, filter f (map g m) == map g (filter (fun x => f (g x)) m).
+    Proof using M M2.
+    intros f g Hf Hg. apply ind.
+    + intros m1 m2 Hm. now rewrite Hm.
+    + intros m x n Hin Hn Hrec. rewrite map_add, 2 filter_add; autoclass; [].
+      destruct (f (g x)).
+      - rewrite map_add; trivial; []. f_equiv. apply Hrec.
+      - apply Hrec.
+    + rewrite map_empty, 2 filter_empty, map_empty; autoclass; reflexivity.
+    Qed.
+
+    Lemma map_partition_fst : forall f g, Proper (equiv ==> Logic.eq) f -> Proper (equiv ==> equiv) g ->
+      forall m, fst (partition f (map g m)) == map g (fst (partition (fun x => f (g x)) m)).
+    Proof using M M2. intros. rewrite 2 partition_spec_fst; try apply map_filter; autoclass. Qed.
+
+    Lemma map_partition_snd : forall f g, Proper (equiv ==> Logic.eq) f -> Proper (equiv ==> equiv) g ->
+      forall m, snd (partition f (map g m)) == map g (snd (partition (fun x => f (g x)) m)).
+    Proof using M M2. intros. rewrite 2 partition_spec_snd; try apply map_filter; autoclass. Qed.
+End map_extensionality_results.
+
   (** **  Function [max] and its properties  **)
   
   (** ***  Function [max_mult] computing the maximal multiplicity  **)
@@ -1448,3 +1456,20 @@ Section MMultisetExtra.
   Qed.
   
 End MMultisetExtra.
+
+Section map_merge.
+  Context {elt elt2 elt3 : Type}.
+  Context `{M : FMultisetsOn elt}.
+  Context `{M2 : FMultisetsOn elt2}.
+  Context `{M3 : FMultisetsOn elt3}.
+
+  Lemma map_merge : forall f : elt2 -> elt3, forall g : elt -> elt2, Proper (equiv ==> equiv) f -> Proper (equiv ==> equiv) g ->
+    forall m, map f (map g m) == map (fun x => f (g x)) m.
+  Proof using M M2 M3.
+  intros f g Hf Hg.
+  apply ind.
+  + repeat intro. now rewrite H2.
+  + intros m x n Hin Hn Hrec. repeat rewrite map_add; refine _. now rewrite Hrec.
+  + now repeat rewrite map_empty.
+  Qed.
+End map_merge.
diff --git a/Util/MMultiset/MMultisetFacts.v b/Util/MMultiset/MMultisetFacts.v
index 91f16a53e4d178d33699aa499b48d34862341811..9e99c3fb0a698b2b1c8766ca69f36233b8574581 100644
--- a/Util/MMultiset/MMultisetFacts.v
+++ b/Util/MMultiset/MMultisetFacts.v
@@ -74,6 +74,7 @@ Section MMultisetFacts.
       | H : id (?x =/= ?y) |- _ => change (x =/= y) in H
     end.
   
+  (* FIXME: Does it work with several [FMultisetsOn] instances? *)
   Ltac msetdec_step := 
     match goal with
       (* Simplifying equalities *)