diff --git a/stdpp/base.v b/stdpp/base.v
index f8105fb370340d9d345f7bb22484d130e70b4742..31f4417eaf7311c11a9ca799dda68183e1c0307a 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1292,7 +1292,7 @@ Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Global Hint Mode Alter - - ! : typeclass_instances.
-Global Instance: Params (@alter) 5 := {}.
+Global Instance: Params (@alter) 4 := {}.
 Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
diff --git a/stdpp/list.v b/stdpp/list.v
index 935a822c3694f8960350a44d9f8af0cd1e3f52f0..d6053261a09a14503f45d861fdf2b8a419a53154 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -39,6 +39,9 @@ Global Instance: Params (@head) 1 := {}.
 Global Instance: Params (@tail) 1 := {}.
 Global Instance: Params (@take) 1 := {}.
 Global Instance: Params (@drop) 1 := {}.
+Global Instance: Params (@Forall) 1 := {}.
+Global Instance: Params (@Exists) 1 := {}.
+Global Instance: Params (@NoDup) 1 := {}.
 
 Global Arguments Permutation {_} _ _ : assert.
 Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
@@ -228,9 +231,11 @@ Global Instance list_bind : MBind list := λ A B f,
 Global Instance list_join: MJoin list :=
   fix go A (ls : list (list A)) : list A :=
   match ls with [] => [] | l :: ls => l ++ @mjoin _ go _ ls end.
+
 Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) :=
   fix go l :=
   match l with [] => mret [] | x :: l => y ← f x; k ← go l; mret (y :: k) end.
+Global Instance: Params (@mapM) 5 := {}.
 
 (** We define stronger variants of the map function that allow the mapped
 function to use the index of the elements. *)
@@ -239,6 +244,7 @@ Fixpoint imap {A B} (f : nat → A → B) (l : list A) : list B :=
   | [] => []
   | x :: l => f 0 x :: imap (f ∘ S) l
   end.
+Global Instance: Params (@imap) 2 := {}.
 
 Definition zipped_map {A B} (f : list A → list A → A → B) :
     list A → list A → list B := fix go l k :=
@@ -246,12 +252,14 @@ Definition zipped_map {A B} (f : list A → list A → A → B) :
   | [] => []
   | x :: k => f l k x :: go (x :: l) k
   end.
+Global Instance: Params (@zipped_map) 2 := {}.
 
 Fixpoint imap2 {A B C} (f : nat → A → B → C) (l : list A) (k : list B) : list C :=
   match l, k with
   | [], _ | _, [] => []
   | x :: l, y :: k => f 0 x y :: imap2 (f ∘ S) l k
   end.
+Global Instance: Params (@imap2) 3 := {}.
 
 Inductive zipped_Forall {A} (P : list A → list A → A → Prop) :
     list A → list A → Prop :=
@@ -2960,9 +2968,6 @@ Section Forall_Exists.
     rewrite Forall_app, Forall_singleton; intros [??]; auto.
   Qed.
 
-  Global Instance Forall_Permutation: Proper ((≡ₚ) ==> (↔)) (Forall P).
-  Proof. intros l1 l2 Hl. rewrite !Forall_forall. by setoid_rewrite Hl. Qed.
-
   Lemma Exists_exists l : Exists P l ↔ ∃ x, x ∈ l ∧ P x.
   Proof.
     split.
@@ -2982,9 +2987,6 @@ Section Forall_Exists.
     Exists P l → (∀ x, P x → Q x) → Exists Q l.
   Proof. intros H ?. induction H; auto. Defined.
 
-  Global Instance Exists_Permutation: Proper ((≡ₚ) ==> (↔)) (Exists P).
-  Proof. intros l1 l2 Hl. rewrite !Exists_exists. by setoid_rewrite Hl. Qed.
-
   Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
   Proof. induction 1; inversion_clear 1; contradiction. Qed.
   Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
@@ -3024,9 +3026,21 @@ Section Forall_Exists.
     | left H => right (Forall_not_Exists _ H)
     | right H => left H
     end.
-
 End Forall_Exists.
 
+Global Instance Forall_Permutation :
+  Proper (pointwise_relation _ (↔) ==> (≡ₚ) ==> (↔)) (@Forall A).
+Proof.
+  intros P1 P2 HP l1 l2 Hl. rewrite !Forall_forall.
+  apply forall_proper; intros x. by rewrite Hl, (HP x).
+Qed.
+Global Instance Exists_Permutation :
+  Proper (pointwise_relation _ (↔) ==> (≡ₚ) ==> (↔)) (@Exists A).
+Proof.
+  intros P1 P2 HP l1 l2 Hl. rewrite !Exists_exists.
+  f_equiv; intros x. by rewrite Hl, (HP x).
+Qed.
+
 Lemma head_filter_Some P `{!∀ x : A, Decision (P x)} l x :
   head (filter P l) = Some x →
   ∃ l1 l2, l = l1 ++ x :: l2 ∧ Forall (λ z, ¬P z) l1.
@@ -3451,9 +3465,9 @@ Section Forall2_proper.
 
   Global Instance: ∀ i, Proper (Forall2 R ==> option_Forall2 R) (lookup i).
   Proof. repeat intro. by apply Forall2_lookup. Qed.
-  Global Instance: ∀ f i,
-    Proper (R ==> R) f → Proper (Forall2 R ==> Forall2 R) (alter f i).
-  Proof. repeat intro. eauto using Forall2_alter. Qed.
+  Global Instance:
+    Proper ((R ==> R) ==> (=) ==> Forall2 R ==> Forall2 R) (alter (M:=list A)).
+  Proof. repeat intro. subst. eauto using Forall2_alter. Qed.
   Global Instance: ∀ i, Proper (R ==> Forall2 R ==> Forall2 R) (insert i).
   Proof. repeat intro. eauto using Forall2_insert. Qed.
   Global Instance: ∀ i,
@@ -3605,8 +3619,11 @@ Proof.
     [by apply list_subseteq_skip|by apply list_subseteq_cons].
 Qed.
 
-Global Instance list_subseteq_Permutation: Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
-Proof. intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk. Qed.
+Global Instance list_subseteq_Permutation:
+  Proper ((≡ₚ) ==> (≡ₚ) ==> (↔)) (⊆@{list A}) .
+Proof.
+  intros l1 l2 Hl k1 k2 Hk. apply forall_proper; intros x. by rewrite Hl, Hk.
+Qed.
 
 Global Program Instance list_subseteq_dec `{!EqDecision A} : RelDecision (⊆@{list A}) :=
   λ xs ys, cast_if (decide (Forall (λ x, x ∈ ys) xs)).
@@ -3656,9 +3673,11 @@ Section setoid.
     Proper (≡) inhabitant →
     Proper ((≡@{list A}) ==> (≡)) (lookup_total i).
   Proof. intros ?. induction i; destruct 1; simpl; auto. Qed.
-  Global Instance list_alter_proper f i :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡@{list A})) (alter f i).
-  Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
+  Global Instance list_alter_proper :
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡@{list A})) alter.
+  Proof.
+    intros f1 f2 Hf i ? <-. induction i; destruct 1; constructor; eauto.
+  Qed.
   Global Instance list_insert_proper i :
     Proper ((≡) ==> (≡) ==> (≡@{list A})) (insert i).
   Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
@@ -3866,6 +3885,10 @@ End find.
 Lemma list_fmap_id {A} (l : list A) : id <$> l = l.
 Proof. induction l; f_equal/=; auto. Qed.
 
+Global Instance list_fmap_proper `{!Equiv A, !Equiv B} :
+  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap.
+Proof. induction 2; csimpl; constructor; auto. Qed.
+
 Section fmap.
   Context {A B : Type} (f : A → B).
   Implicit Types l : list A.
@@ -3878,9 +3901,6 @@ Section fmap.
   Lemma list_fmap_equiv_ext `{!Equiv B} (g : A → B) l :
     (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
   Proof. induction l; constructor; auto. Qed.
-  Global Instance list_fmap_proper `{!Equiv A, !Equiv B} :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f).
-  Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
 
   Global Instance fmap_inj: Inj (=) (=) f → Inj (=@{list A}) (=) (fmap f).
   Proof.
@@ -4077,6 +4097,13 @@ Proof.
   - apply IH. intros. eapply Hunique; rewrite ?elem_of_cons; eauto.
 Qed.
 
+Global Instance list_omap_proper `{!Equiv A, !Equiv B} :
+  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) omap.
+Proof.
+  intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
+  destruct (Hf _ _ Hx); by repeat f_equiv.
+Qed.
+
 Section omap.
   Context {A B : Type} (f : A → option B).
   Implicit Types l : list A.
@@ -4094,12 +4121,6 @@ Section omap.
     induction 1 as [|x y l l' Hfg ? IH]; [done|].
     csimpl. rewrite Hfg. destruct (g y); [|done]. by f_equal.
   Qed.
-  Global Instance list_omap_proper `{!Equiv A, !Equiv B} :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (omap f).
-  Proof.
-    intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
-    destruct (Hf _ _ Hx); by repeat f_equiv.
-  Qed.
   Lemma elem_of_list_omap l y : y ∈ omap f l ↔ ∃ x, x ∈ l ∧ f x = Some y.
   Proof.
     split.
@@ -4119,6 +4140,10 @@ Section omap.
   Proof. by destruct mx. Qed.
 End omap.
 
+Global Instance list_bind_proper `{!Equiv A, !Equiv B} :
+  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) mbind.
+Proof. induction 2; csimpl; constructor || f_equiv; auto. Qed.
+
 Section bind.
   Context {A B : Type} (f : A → list B).
 
@@ -4128,9 +4153,6 @@ Section bind.
   Lemma Forall_bind_ext (g : A → list B) (l : list A) :
     Forall (λ x, f x = g x) l → l ≫= f = l ≫= g.
   Proof. by induction 1; f_equal/=. Qed.
-  Global Instance list_bind_proper `{!Equiv A, !Equiv B} :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
-  Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
   Global Instance bind_sublist: Proper (sublist ==> sublist) (mbind f).
   Proof.
     induction 1; simpl; auto;
@@ -4180,11 +4202,13 @@ Section bind.
   Proof. induction 1; csimpl; auto using Forall2_app. Qed.
 End bind.
 
+Global Instance list_join_proper `{!Equiv A} :
+  Proper ((≡) ==> (≡@{list A})) mjoin.
+Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
+
 Section ret_join.
   Context {A : Type}.
 
-  Global Instance list_join_proper `{!Equiv A} : Proper ((≡) ==> (≡)) (mjoin (A:=A)).
-  Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
   Lemma list_join_bind (ls : list (list A)) : mjoin ls = ls ≫= id.
   Proof. by induction ls; f_equal/=. Qed.
   Global Instance join_Permutation : Proper ((≡ₚ@{list A}) ==> (≡ₚ)) mjoin.
@@ -4211,14 +4235,17 @@ Section ret_join.
   Proof. induction 1; simpl; auto using Forall2_app. Qed.
 End ret_join.
 
+Global Instance mapM_proper `{!Equiv A, !Equiv B} :
+  Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{option (list B)})) mapM.
+Proof.
+  induction 2; csimpl; repeat (f_equiv || constructor || intro || auto).
+Qed.
+
 Section mapM.
   Context {A B : Type} (f : A → option B).
 
   Lemma mapM_ext (g : A → option B) l : (∀ x, f x = g x) → mapM f l = mapM g l.
   Proof. intros Hfg. by induction l as [|?? IHl]; simpl; rewrite ?Hfg, ?IHl. Qed.
-  Global Instance mapM_proper `{!Equiv A, !Equiv B} :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
-  Proof. induction 2; simpl; [solve_proper|constructor]. Qed.
 
   Lemma Forall2_mapM_ext (g : A → option B) l k :
     Forall2 (λ x y, f x = g y) l k → mapM f l = mapM g k.
@@ -4285,18 +4312,22 @@ End mapM.
 Lemma imap_const {A B} (f : A → B) l : imap (const f) l = f <$> l.
 Proof. induction l; f_equal/=; auto. Qed.
 
+Global Instance imap_proper `{!Equiv A, !Equiv B} :
+  Proper (pointwise_relation _ ((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B}))
+         imap.
+Proof.
+  intros f f' Hf l l' Hl. revert f f' Hf.
+  induction Hl as [|x1 x2 l1 l2 ?? IH]; intros f f' Hf; simpl; constructor.
+  - by apply Hf.
+  - apply IH. intros i y y' ?; simpl. by apply Hf.
+Qed.
+
 Section imap.
   Context {A B : Type} (f : nat → A → B).
 
   Lemma imap_ext g l :
     (∀ i x, l !! i = Some x → f i x = g i x) → imap f l = imap g l.
   Proof. revert f g; induction l as [|x l IH]; intros; f_equal/=; eauto. Qed.
-  Global Instance imap_proper `{!Equiv A, !Equiv B} :
-    (∀ i, Proper ((≡) ==> (≡)) (f i)) → Proper ((≡) ==> (≡)) (imap f).
-  Proof.
-    intros Hf l1 l2 Hl. revert f Hf.
-    induction Hl; intros f Hf; simpl; [constructor|repeat f_equiv; naive_solver].
-  Qed.
 
   Lemma imap_nil : imap f [] = [].
   Proof. done. Qed.
@@ -4507,6 +4538,14 @@ Lemma foldl_fmap {A B C} (f : A → B → A) x (l : list C) g :
 Proof. revert x. induction l; f_equal/=; auto. Qed.
 
 (** ** Properties of the [zip_with] and [zip] functions *)
+Global Instance zip_with_proper `{!Equiv A, !Equiv B, !Equiv C} :
+  Proper (((≡) ==> (≡) ==> (≡)) ==>
+          (≡@{list A}) ==> (≡@{list B}) ==> (≡@{list C})) zip_with.
+Proof.
+  intros f1 f2 Hf. induction 1; destruct 1; simpl; [constructor..|].
+  f_equiv; [|by auto]. by apply Hf.
+Qed.
+
 Section zip_with.
   Context {A B C : Type} (f : A → B → C).
   Implicit Types x : A.
@@ -4514,9 +4553,6 @@ Section zip_with.
   Implicit Types l : list A.
   Implicit Types k : list B.
 
-  Global Instance zip_with_proper `{!Equiv A, !Equiv B, !Equiv C} :
-    Proper ((≡) ==> (≡) ==> (≡)) f → Proper ((≡) ==> (≡) ==> (≡)) (zip_with f).
-  Proof. induction 2; destruct 1; simpl; [constructor..|repeat f_equiv; auto]. Qed.
   Lemma zip_with_nil_r l : zip_with f l [] = [].
   Proof. by destruct l. Qed.
   Lemma zip_with_app l1 l2 k1 k2 :
diff --git a/tests/proper.v b/tests/proper.v
index 423731fc5ee89a39e1887368bdc66ec5527089a3..36249631f6cb23b9d39568f83dbf05f19e6f391e 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -85,38 +85,42 @@ Section map_tests.
   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} :
+  Global Instance map_alter_proper_test (f : A → A) i :
+    Proper ((≡) ==> (≡)) f →
+    Proper ((≡) ==> (≡)) (alter (M:=M A) f i).
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_zip_proper_test `{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) :
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_zip_with_proper_test `{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) :
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_fmap_proper_test `{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) :
+  Proof. apply _. Restart. solve_proper. Abort.
+  Global Instance map_omap_proper_test `{Equiv B} (f : A → option B) :
     Proper ((≡) ==> (≡)) f →
     Proper ((≡) ==> (≡@{M _})) (omap f).
-  Proof. solve_proper. Qed.
+  Proof. apply _. Restart. solve_proper. Abort.
 End map_tests.
 
+(** And similarly for lists *)
+Global Instance list_alter_proper_test `{!Equiv A} (f : A → A) i :
+  Proper ((≡) ==> (≡)) f →
+  Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+Proof. apply _. Restart. solve_proper. Abort.
+Global Instance list_fmap_proper_test `{!Equiv A, !Equiv B} (f : A → B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f).
+Proof. apply _. Restart. solve_proper. Abort.
+Global Instance list_bind_proper_test `{!Equiv A, !Equiv B} (f : A → list B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mbind f).
+Proof. apply _. Restart. solve_proper. Abort.
+Global Instance mapM_proper_test `{!Equiv A, !Equiv B} (f : A → option B) :
+  Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (mapM f).
+Proof. apply _. Restart. solve_proper. Abort.
+
 Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
   X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
 Proof. intros H1 H2. by rewrite H1, <-H2. Qed.