diff --git a/tests/solve_proper.ref b/tests/proper.ref
similarity index 100%
rename from tests/solve_proper.ref
rename to tests/proper.ref
diff --git a/tests/proper.v b/tests/proper.v
new file mode 100644
index 0000000000000000000000000000000000000000..5efcdbce091f2141489f3ee16a06eeabf75ea862
--- /dev/null
+++ b/tests/proper.v
@@ -0,0 +1,64 @@
+From stdpp Require Import prelude fin_maps.
+
+(** Some tests for solve_proper. *)
+Section tests.
+  Context {A B : Type} `{!Equiv A, !Equiv B}.
+  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
+  Context `{!Proper ((≡) ==> (≡)) foo,
+            !Proper ((≡) ==> (≡)) bar,
+            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
+
+  Definition test1 (x : A) := baz (bar (foo x)) x.
+  Goal Proper ((≡) ==> (≡)) test1.
+  Proof. solve_proper. Qed.
+
+  Definition test2 (b : bool) (x : A) :=
+    if b then bar (foo x) else bar x.
+  Goal ∀ b, Proper ((≡) ==> (≡)) (test2 b).
+  Proof. solve_proper. Qed.
+
+  Definition test3 (f : nat → A) :=
+    baz (bar (f 0)) (f 2).
+  Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3.
+  Proof. solve_proper. Qed.
+End tests.
+
+Section map_tests.
+  Context `{FinMap K M} `{Equiv A}.
+
+  (** For higher-order functions on maps (like [map_with_with], [fmap], etc)
+  we use "higher-order [Proper] instances" [Proper ((≡) ==> (≡)) ==> ...)]
+  that also allow the function to differ. We test that we can derive simpler
+  [Proper]s for a fixed function using both type class inference ([apply _])
+  and std++'s [solve_proper] tactic. *)
+  Global Instance map_zip_proper_test1 `{Equiv B} :
+    Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
+  Proof. apply _. Abort.
+  Global Instance map_zip_proper_test2 `{Equiv B} :
+    Proper ((≡@{M A}) ==> (≡@{M B}) ==> (≡@{M (A * B)})) map_zip.
+  Proof. solve_proper. Abort.
+  Global Instance map_zip_with_proper_test1 `{Equiv B, Equiv C} (f : A → B → C) :
+    Proper ((≡) ==> (≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Proof. apply _. Qed.
+  Global Instance map_zip_with_proper_test2 `{Equiv B, Equiv C} (f : A → B → C) :
+    Proper ((≡) ==> (≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+  Proof. solve_proper. Abort.
+  Global Instance map_fmap_proper_test1 `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Proof. apply _. Qed.
+  Global Instance map_fmap_proper_test2 `{Equiv B} (f : A → B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Proof. solve_proper. Qed.
+  Global Instance map_omap_proper_test1 `{Equiv B} (f : A → option B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (omap f).
+  Proof. apply _. Qed.
+  Global Instance map_omap_proper_test2 `{Equiv B} (f : A → option B) :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡@{M _})) (omap f).
+  Proof. solve_proper. Qed.
+End map_tests.
diff --git a/tests/solve_proper.v b/tests/solve_proper.v
deleted file mode 100644
index d4e4d665e7c1cadd9fc52ac7892b785c21c9e8a7..0000000000000000000000000000000000000000
--- a/tests/solve_proper.v
+++ /dev/null
@@ -1,24 +0,0 @@
-From stdpp Require Import prelude.
-
-(** Some tests for solve_proper. *)
-Section tests.
-  Context {A B : Type} `{!Equiv A, !Equiv B}.
-  Context (foo : A → A) (bar : A → B) (baz : B → A → A).
-  Context `{!Proper ((≡) ==> (≡)) foo,
-            !Proper ((≡) ==> (≡)) bar,
-            !Proper ((≡) ==> (≡) ==> (≡)) baz}.
-
-  Definition test1 (x : A) := baz (bar (foo x)) x.
-  Goal Proper ((≡) ==> (≡)) test1.
-  Proof. solve_proper. Qed.
-
-  Definition test2 (b : bool) (x : A) :=
-    if b then bar (foo x) else bar x.
-  Goal ∀ b, Proper ((≡) ==> (≡)) (test2 b).
-  Proof. solve_proper. Qed.
-
-  Definition test3 (f : nat → A) :=
-    baz (bar (f 0)) (f 2).
-  Goal Proper (pointwise_relation nat (≡) ==> (≡)) test3.
-  Proof. solve_proper. Qed.
-End tests.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index a109d8580ba00789812d43ff54d621aae9e36fe2..6dde00f567ba7e0a00942a4b4a2aecf512de197d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -166,6 +166,8 @@ Context `{FinMap K M}.
 Section setoid.
   Context `{Equiv A}.
 
+  Lemma map_equiv_iff (m1 m2 : M A) : m1 ≡ m2 ↔ ∀ i, m1 !! i ≡ m2 !! i.
+  Proof. done. Qed.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
     split; [intros Hm; apply map_eq; intros i|intros ->].
@@ -175,6 +177,9 @@ Section setoid.
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
+  Lemma map_equiv_lookup_r (m1 m2 : M A) i y :
+    m1 ≡ m2 → m2 !! i = Some y → ∃ x, m1 !! i = Some x ∧ x ≡ y.
+  Proof. generalize (equiv_Some_inv_r (m1 !! i) (m2 !! i) y); naive_solver. Qed.
 
   Global Instance map_equivalence : Equivalence (≡@{A}) → Equivalence (≡@{M A}).
   Proof.
@@ -190,7 +195,7 @@ Section setoid.
   Proof. by intros m1 m2 Hm. Qed.
   Global Instance lookup_total_proper (i : K) `{!Inhabited A} :
     Proper (≡@{A}) inhabitant →
-    Proper ((≡@{M A}) ==> (≡)) (lookup_total i).
+    Proper ((≡@{M A}) ==> (≡)) (.!!! i).
   Proof.
     intros ? m1 m2 Hm. unfold lookup_total, map_lookup_total.
     apply from_option_proper; auto. by intros ??.
@@ -232,18 +237,48 @@ Section setoid.
     intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
+  Global Instance intersection_with_proper :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) intersection_with.
+  Proof.
+    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    by do 2 destruct 1; first [apply Hf | constructor].
+  Qed.
+  Global Instance difference_with_proper :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) difference_with.
+  Proof.
+    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    by do 2 destruct 1; first [apply Hf | constructor].
+  Qed.
+  Global Instance union_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) union.
+  Proof. apply union_with_proper; solve_proper. Qed.
+  Global Instance intersection_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) intersection.
+  Proof. apply intersection_with_proper; solve_proper. Qed.
+  Global Instance difference_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) difference.
+  Proof. apply difference_with_proper. constructor. Qed.
 
-  Global Instance map_fmap_proper `{Equiv B} (f : A → B) :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{M _})) (fmap f).
+  Global Instance map_zip_with_proper `{Equiv B, Equiv C} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B}) ==> (≡@{M C}))
+      map_zip_with.
   Proof.
-    intros ? m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
+    intros f1 f2 Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
+    destruct 1; destruct 1; repeat f_equiv; constructor || by apply Hf.
   Qed.
-  Global Instance map_zip_with_proper `{Equiv B, Equiv C} (f : A → B → C) :
-    Proper ((≡) ==> (≡) ==> (≡)) f →
-    Proper ((≡) ==> (≡) ==> (≡)) (map_zip_with (M:=M) f).
+
+  Global Instance map_disjoint_proper :
+    Proper ((≡@{M A}) ==> (≡@{M A}) ==> iff) map_disjoint.
   Proof.
-    intros Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
-    destruct 1; destruct 1; repeat f_equiv; constructor || done.
+    intros m1 m1' Hm1 m2 m2' Hm2; split;
+      intros Hm i; specialize (Hm i); by destruct (Hm1 i), (Hm2 i).
+  Qed.
+  Global Instance map_fmap_proper `{Equiv B} :
+    Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) fmap.
+  Proof.
+    intros f f' Hf m m' ? k; rewrite !lookup_fmap. by apply option_fmap_proper.
+  Qed.
+  Global Instance map_omap_proper `{Equiv B} :
+    Proper (((≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B})) omap.
+  Proof.
+    intros f f' ? m m' ? k; rewrite !lookup_omap. by apply option_bind_proper.
   Qed.
 End setoid.
 
@@ -642,6 +677,14 @@ Proof.
   - rewrite lookup_singleton in Heq. naive_solver.
   - rewrite lookup_singleton_ne in Heq by done. naive_solver.
 Qed.
+Global Instance map_singleton_equiv_inj `{Equiv A} :
+  Inj2 (=) (≡) (≡) (singletonM (M:=M A)).
+Proof.
+  intros i1 x1 i2 x2 Heq. specialize (Heq i1).
+  rewrite lookup_singleton in Heq. destruct (decide (i1 = i2)) as [->|].
+  - rewrite lookup_singleton in Heq. apply (inj _) in Heq. naive_solver.
+  - rewrite lookup_singleton_ne in Heq by done. inversion Heq.
+Qed.
 
 Lemma map_non_empty_singleton {A} i (x : A) : {[i := x]} ≠ (∅ : M A).
 Proof.
@@ -681,6 +724,12 @@ Proof.
   intros ? m1 m2 Hm. apply map_eq; intros i.
   apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
 Qed.
+Global Instance map_fmap_equiv_inj `{Equiv A, Equiv B} (f : A → B) :
+  Inj (≡) (≡) f → Inj (≡@{M A}) (≡@{M B}) (fmap f).
+Proof.
+  intros ? m1 m2 Hm i. apply (inj (fmap (M:=option) f)).
+  rewrite <-!lookup_fmap. by apply lookup_proper.
+Qed.
 
 Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
   (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
diff --git a/theories/option.v b/theories/option.v
index 412cd5ce1c09b69bc6041e9cdbfd138cda585499..82b1387aedd65b27e5d5fd4020ff8fef91776b8e 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -145,8 +145,8 @@ Section setoids.
 
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
-  Global Instance from_option_proper {B} (R : relation B) (f : A → B) :
-    Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f).
+  Global Instance from_option_proper {B} (R : relation B) :
+    Proper (((≡@{A}) ==> R) ==> R ==> (≡) ==> R) from_option.
   Proof. destruct 3; simpl; auto. Qed.
 End setoids.
 
@@ -179,6 +179,9 @@ Global Instance option_guard: MGuard option := λ P dec A f,
 Global Instance option_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{option A}) (=@{option B}) (fmap f).
 Proof. intros ? [x1|] [x2|] [=]; naive_solver. Qed.
+Global Instance option_fmap_equiv_inj `{Equiv A, Equiv B} (f : A → B) :
+  Inj (≡) (≡) f → Inj (≡@{option A}) (≡@{option B}) (fmap f).
+Proof. intros ? [x1|] [x2|]; inversion 1; subst; constructor; by apply (inj _). Qed.
 
 Lemma fmap_is_Some {A B} (f : A → B) mx : is_Some (f <$> mx) ↔ is_Some mx.
 Proof. unfold is_Some; destruct mx; naive_solver. Qed.
@@ -243,10 +246,10 @@ Proof. by destruct mx. Qed.
 Global Instance option_fmap_proper `{Equiv A, Equiv B} :
   Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) fmap.
 Proof. destruct 2; constructor; auto. Qed.
-Global Instance option_mbind_proper `{Equiv A, Equiv B} :
+Global Instance option_bind_proper `{Equiv A, Equiv B} :
   Proper (((≡) ==> (≡)) ==> (≡@{option A}) ==> (≡@{option B})) mbind.
 Proof. destruct 2; simpl; try constructor; auto. Qed.
-Global Instance option_mjoin_proper `{Equiv A} :
+Global Instance option_join_proper `{Equiv A} :
   Proper ((≡) ==> (≡@{option (option A)})) mjoin.
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.