diff --git a/stdpp/base.v b/stdpp/base.v
index 26fff8e206da17cb4a552bf1e09f482410e670c5..f9d6a09943b9787b4da5a154aff89aafebe4b120 100644
--- a/stdpp/base.v
+++ b/stdpp/base.v
@@ -1194,30 +1194,44 @@ Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
-Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
+Class MRet' (A MA : Type) := mret: A → MA.
+Global Notation MRet M := (∀ A, MRet' A (M A)).
 Global Arguments mret {_ _ _} _ : assert.
 Global Instance: Params (@mret) 3 := {}.
-Global Hint Mode MRet ! : typeclass_instances.
+Global Hint Mode MRet' - ! : typeclass_instances.
 
-Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
+Class MBind' (A MA MB : Type) := mbind : (A → MB) → MA → MB.
+Global Notation MBind M := (∀ A B, MBind' A (M A) (M B)).
 Global Arguments mbind {_ _ _ _} _ !_ / : assert.
 Global Instance: Params (@mbind) 4 := {}.
-Global Hint Mode MBind ! : typeclass_instances.
-
-Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
+(** [MA] and [MB] should have the same type constructor at the head,
+so one determines the other and it is fine if one of them is an evar.
+Also [MA] should determine [A]. The same applies to the other
+typeclasses below. *)
+Global Hint Mode MBind' - - ! : typeclass_instances.
+Global Hint Mode MBind' - ! - : typeclass_instances.
+
+Class MJoin' (MA MMA : Type) := mjoin: MMA → MA.
+(* TODO: Can we get rid of the inconsistent-scopes warning in a better way than %type? *)
+Global Notation MJoin M := (∀ A, MJoin' (M A) (M (M A))%type).
 Global Arguments mjoin {_ _ _} !_ / : assert.
 Global Instance: Params (@mjoin) 3 := {}.
-Global Hint Mode MJoin ! : typeclass_instances.
-
-Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
-Global Arguments fmap {_ _ _ _} _ !_ / : assert.
-Global Instance: Params (@fmap) 4 := {}.
-Global Hint Mode FMap ! : typeclass_instances.
-
-Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
-Global Arguments omap {_ _ _ _} _ !_ / : assert.
-Global Instance: Params (@omap) 4 := {}.
-Global Hint Mode OMap ! : typeclass_instances.
+Global Hint Mode MJoin' ! - : typeclass_instances.
+Global Hint Mode MJoin' - ! : typeclass_instances.
+
+Class FMap' (A B MA MB : Type) := fmap : (A → B) → MA → MB.
+Global Notation FMap M := (∀ A B, FMap' A B (M A) (M B)).
+Global Arguments fmap {_ _ _ _ _} _ !_ / : assert.
+Global Instance: Params (@fmap) 5 := {}.
+Global Hint Mode FMap' - - ! - : typeclass_instances.
+Global Hint Mode FMap' - - - ! : typeclass_instances.
+
+Class OMap' (A B MA MB : Type) := omap: (A → option B) → MA → MB.
+Global Notation OMap M := (∀ A B, OMap' A B (M A) (M B)).
+Global Arguments omap {_ _ _ _ _} _ !_ / : assert.
+Global Instance: Params (@omap) 5 := {}.
+Global Hint Mode OMap' - - ! - : typeclass_instances.
+Global Hint Mode OMap' - - - ! : typeclass_instances.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
 Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
@@ -1235,20 +1249,21 @@ Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
 Notation "x ;; z" := (x ≫= λ _, z)
   (at level 100, z at level 200, only parsing, right associativity): stdpp_scope.
 
-Notation "ps .*1" := (fmap (M:=list) fst ps)
+Notation "ps .*1" := (fmap (MA:=list _) fst ps)
   (at level 2, left associativity, format "ps .*1").
-Notation "ps .*2" := (fmap (M:=list) snd ps)
+Notation "ps .*2" := (fmap (MA:=list _) snd ps)
   (at level 2, left associativity, format "ps .*2").
 
 (** For any monad that has a builtin way to throw an exception/error *)
-Class MThrow (E : Type) (M : Type → Type) := mthrow : ∀ {A}, E → M A.
-Global Arguments mthrow {_ _ _ _} _ : assert.
-Global Instance: Params (@mthrow) 4 := {}.
-Global Hint Mode MThrow ! ! : typeclass_instances.
+Class MThrow' (E MA : Type) := mthrow : E → MA.
+Notation MThrow E M := (∀ A, MThrow' E (M A)).
+Global Arguments mthrow {_ _ _} _ : assert.
+Global Instance: Params (@mthrow) 3 := {}.
+Global Hint Mode MThrow' ! ! : typeclass_instances.
 
 (** We use unit as the error content for monads that can only report an error
     without any payload like an option *)
-Global Notation MFail := (MThrow ()).
+Global Notation MFail M := (MThrow () M).
 Global Notation mfail := (mthrow ()).
 
 Definition guard_or {E} (e : E) `{MThrow E M, MRet M} P `{Decision P} : M P :=
@@ -1404,11 +1419,14 @@ Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
-Class Merge (M : Type → Type) :=
-  merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
-Global Hint Mode Merge ! : typeclass_instances.
-Global Instance: Params (@merge) 4 := {}.
-Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Class Merge' (A B C MA MB MC : Type) :=
+  merge: (option A → option B → option C) → MA → MB → MC.
+Global Notation Merge M := (∀ A B C, Merge' A B C (M A) (M B) (M C)).
+Global Hint Mode Merge' - - - ! - - : typeclass_instances.
+Global Hint Mode Merge' - - - - ! - : typeclass_instances.
+Global Hint Mode Merge' - - - - - ! : typeclass_instances.
+Global Instance: Params (@merge) 7 := {}.
+Global Arguments merge _ _ _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
@@ -1617,4 +1635,4 @@ Global Arguments infinite_fresh : simpl never.
 Class Half A := half: A → A.
 Global Hint Mode Half ! : typeclass_instances.
 Notation "½" := half (format "½") : stdpp_scope.
-Notation "½*" := (fmap (M:=list) half) : stdpp_scope.
+Notation "½*" := (fmap (MA:=list _) half) : stdpp_scope.
diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index af749f006febe52203581172daecec546398d45e..73f40a7f449a386d7d384a23ffadfb06b7d7f455 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -800,7 +800,7 @@ Global Instance map_fmap_inj {A B} (f : A → B) :
   Inj (=) (=) f → Inj (=@{M A}) (=@{M B}) (fmap f).
 Proof.
   intros ? m1 m2 Hm. apply map_eq; intros i.
-  apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
+  apply (inj (fmap (MA:=option A) f)). by rewrite <-!lookup_fmap, Hm.
 Qed.
 
 Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
@@ -3576,7 +3576,7 @@ Section setoid.
   Global Instance map_fmap_equiv_inj `{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)).
+    intros ? m1 m2 Hm i. apply (inj (fmap (MA:=option A) f)).
     rewrite <-!lookup_fmap. by apply Hm.
   Qed.
 
diff --git a/stdpp/list.v b/stdpp/list.v
index 9b25e6d9dc04d99d29a8c2dfb80b33fcca4e85bc..79e0156b54d70cb826a0111dcb226f048472c96f 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -222,7 +222,7 @@ Global Instance list_bind : MBind list := λ A B f,
   fix go (l : list A) := match l with [] => [] | x :: l => f x ++ go l end.
 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.
+  match ls with [] => [] | l :: ls => l ++ @mjoin _ _ (go A) ls end.
 
 Definition mapM `{MBind M, MRet M} {A B} (f : A → M B) : list A → M (list B) :=
   fix go l :=
@@ -4150,7 +4150,7 @@ Section fmap.
 
   Lemma NoDup_fmap_1 l : NoDup (f <$> l) → NoDup l.
   Proof.
-    induction l; simpl; inv 1; constructor; auto.
+    induction l; csimpl; inv 1; constructor; auto.
     rewrite elem_of_list_fmap in *. naive_solver.
   Qed.
   Lemma NoDup_fmap_2 `{!Inj (=) (=) f} l : NoDup l → NoDup (f <$> l).
@@ -4362,7 +4362,7 @@ Section ret_join.
   Proof. by induction ls; f_equal/=. Qed.
   Global Instance join_Permutation : Proper ((≡ₚ@{list A}) ==> (≡ₚ)) mjoin.
   Proof. intros ?? E. by rewrite !list_join_bind, E. Qed.
-  Lemma elem_of_list_ret (x y : A) : x ∈ @mret list _ A y ↔ x = y.
+  Lemma elem_of_list_ret (x y : A) : x ∈ @mret A (list A) _ y ↔ x = y.
   Proof. apply elem_of_list_singleton. Qed.
   Lemma elem_of_list_join (x : A) (ls : list (list A)) :
     x ∈ mjoin ls ↔ ∃ l : list A, x ∈ l ∧ l ∈ ls.
diff --git a/stdpp/natmap.v b/stdpp/natmap.v
index 59c6e5d773476e8d163cb2fe9f0f40804d52a8be..661bb8b2a7b65b7e2a3ec585f550b15948961da1 100644
--- a/stdpp/natmap.v
+++ b/stdpp/natmap.v
@@ -109,7 +109,7 @@ Proof.
 Qed.
 
 Definition natmap_fmap_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
-  fmap (fmap (M:=option) f).
+  fmap (fmap (MA:=option A) f).
 Lemma natmap_fmap_wf {A B} (f : A → B) l :
   natmap_wf l → natmap_wf (natmap_fmap_raw f l).
 Proof.
diff --git a/stdpp/option.v b/stdpp/option.v
index 02e02016164b7daf5dacf534dc090b112b93d82a..2962dcd6336aeab8c3a44b184a652e325e94214f 100644
--- a/stdpp/option.v
+++ b/stdpp/option.v
@@ -439,12 +439,12 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
       assert (mx = Some x) as H by tac
     | assert (mx = None) as H by tac ]
   in repeat match goal with
-  | H : context [@mret _ _ ?A] |- _ =>
-     change (@mret _ _ A) with (@Some A) in H
-  | |- context [@mret _ _ ?A] => change (@mret _ _ A) with (@Some A)
-  | H : context [mbind (M:=option) (A:=?A) ?f ?mx] |- _ =>
+  | H : context [@mret ?A (option _) _] |- _ =>
+     change (@mret A (option _) _) with (@Some A) in H
+  | |- context [@mret ?A (option _) _] => change (@mret A (option _) _) with (@Some A)
+  | H : context [mbind (A:=?A) (MA:=option ?A) (MB:=option ?B) ?f ?mx] |- _ =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
-  | H : context [fmap (M:=option) (A:=?A) ?f ?mx] |- _ =>
+  | H : context [fmap (A:=?A) (MA:=option ?A) (MB:=option ?B) ?f ?mx] |- _ =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
   | H : context [from_option (A:=?A) _ _ ?mx] |- _ =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
@@ -453,9 +453,9 @@ Tactic Notation "simpl_option" "by" tactic3(tac) :=
     | option ?A =>
       let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx in H; clear Hx
     end
-  | |- context [mbind (M:=option) (A:=?A) ?f ?mx] =>
+  | |- context [mbind (MA:=option ?A) (MB:=option ?B) (A:=?A) ?f ?mx] =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
-  | |- context [fmap (M:=option) (A:=?A) ?f ?mx] =>
+  | |- context [fmap (A:=?A) (MA:=option ?A) (MB:=option ?B) ?f ?mx] =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
   | |- context [from_option (A:=?A) _ _ ?mx] =>
     let Hx := fresh in assert_Some_None A mx Hx; rewrite Hx; clear Hx
@@ -486,22 +486,22 @@ Tactic Notation "simplify_option_eq" "by" tactic3(tac) :=
   | _ : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
   | _ : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
   | H : _ ∪ _ = Some _ |- _ => apply union_Some in H; destruct H
-  | H : mbind (M:=option) ?f ?mx = ?my |- _ =>
+  | H : mbind (MA:=option ?A) (MB:=option ?B) (A:=?A) ?f ?mx = ?my |- _ =>
     match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match my with Some _ => idtac | None => idtac | _ => fail 1 end;
     let x := fresh in destruct mx as [x|] eqn:?;
       [change (f x = my) in H|change (None = my) in H]
-  | H : ?my = mbind (M:=option) ?f ?mx |- _ =>
+  | H : ?my = mbind (MA:=option ?A) (MB:=option ?B) (A:=?A) ?f ?mx |- _ =>
     match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match my with Some _ => idtac | None => idtac | _ => fail 1 end;
     let x := fresh in destruct mx as [x|] eqn:?;
       [change (my = f x) in H|change (my = None) in H]
-  | H : fmap (M:=option) ?f ?mx = ?my |- _ =>
+  | H : fmap (A:=?A) (MA:=option ?A) (MB:=option ?B) ?f ?mx = ?my |- _ =>
     match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match my with Some _ => idtac | None => idtac | _ => fail 1 end;
     let x := fresh in destruct mx as [x|] eqn:?;
       [change (Some (f x) = my) in H|change (None = my) in H]
-  | H : ?my = fmap (M:=option) ?f ?mx |- _ =>
+  | H : ?my = fmap (A:=?A) (MA:=option ?A) (MB:=option ?B) ?f ?mx |- _ =>
     match mx with Some _ => fail 1 | None => fail 1 | _ => idtac end;
     match my with Some _ => idtac | None => idtac | _ => fail 1 end;
     let x := fresh in destruct mx as [x|] eqn:?;
diff --git a/stdpp/sets.v b/stdpp/sets.v
index a681d7c5d44cee30e62de36281636503d1b7060a..e60e07a88e7a90743bdb2b61035e0c2757ed219c 100644
--- a/stdpp/sets.v
+++ b/stdpp/sets.v
@@ -70,19 +70,19 @@ Section setoids_monad.
   Context `{MonadSet M}.
 
   Global Instance set_fmap_proper {A B} :
-    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
+    Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap A B (M A) (M B) _).
   Proof.
     intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_fmap. f_equiv; intros z.
     by rewrite HX, Hf.
   Qed.
   Global Instance set_bind_proper {A B} :
-    Proper (pointwise_relation _ (≡) ==> (≡) ==> (≡)) (@mbind M _ A B).
+    Proper (pointwise_relation _ (≡) ==> (≡) ==> (≡)) (@mbind A (M A) (M B) _).
   Proof.
     intros f1 f2 Hf X1 X2 HX x. rewrite !elem_of_bind. f_equiv; intros z.
     by rewrite HX, (Hf z).
   Qed.
   Global Instance set_join_proper {A} :
-    Proper ((≡) ==> (≡)) (@mjoin M _ A).
+    Proper ((≡) ==> (≡)) (@mjoin (M A) (M (M A)) _).
   Proof.
     intros X1 X2 HX x. rewrite !elem_of_join. f_equiv; intros z. by rewrite HX.
   Qed.
@@ -254,7 +254,7 @@ Section set_unfold_monad.
   Context `{MonadSet M}.
 
   Global Instance set_unfold_ret {A} (x y : A) :
-    SetUnfoldElemOf x (mret (M:=M) y) (x = y).
+    SetUnfoldElemOf x (mret (MA:=M A) y) (x = y).
   Proof. constructor; apply elem_of_ret. Qed.
   Global Instance set_unfold_bind {A B} (f : A → M B) X (P Q : A → Prop) x :
     (∀ y, SetUnfoldElemOf y X (P y)) → (∀ y, SetUnfoldElemOf x (f y) (Q y)) →
@@ -1056,13 +1056,13 @@ Section set_monad.
   Context `{MonadSet M}.
 
   Global Instance set_fmap_mono {A B} :
-    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
+    Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap A B (M A) (M B) _).
   Proof. intros f g ? X Y ?; set_solver by eauto. Qed.
   Global Instance set_bind_mono {A B} :
-    Proper (pointwise_relation _ (⊆) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
+    Proper (pointwise_relation _ (⊆) ==> (⊆) ==> (⊆)) (@mbind A (M A) (M B) _).
   Proof. unfold respectful, pointwise_relation; intros f g Hfg X Y ?. set_solver. Qed.
   Global Instance set_join_mono {A} :
-    Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
+    Proper ((⊆) ==> (⊆)) (@mjoin (M A) (M (M A)) _).
   Proof. intros X Y ?; set_solver. Qed.
 
   Lemma set_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
diff --git a/stdpp/tactics.v b/stdpp/tactics.v
index f838bf02249f22bd8a5e01f2f62d1a89d7071314..4ba8dc509f620fd7d85527f823375a61eaa7517e 100644
--- a/stdpp/tactics.v
+++ b/stdpp/tactics.v
@@ -182,11 +182,11 @@ Tactic Notation "case_guard" "as" ident(Hx) :=
   match goal with
   | H : context C [@guard_or ?E ?e ?M ?T ?R ?P ?dec] |- _ =>
       change (@guard_or E e M T R P dec) with (
-        match @decide P dec with left H' => @mret M R P H' | _ => @mthrow E M T P e end) in *;
+        match @decide P dec with left H' => @mret P (M P) (R P) H' | _ => @mthrow E (M P) (T P) e end) in *;
       destruct_decide (@decide P dec) as Hx
   | |- context C [@guard_or ?E ?e ?M ?T ?R ?P ?dec] =>
       change (@guard_or E e M T R P dec) with (
-        match @decide P dec with left H' => @mret M R P H' | _ => @mthrow E M T P e end) in *;
+        match @decide P dec with left H' => @mret P (M P) (R P) H' | _ => @mthrow E (M P) (T P) e end) in *;
       destruct_decide (@decide P dec) as Hx
   end.
 Tactic Notation "case_guard" :=
@@ -295,15 +295,15 @@ Ltac fold_classes :=
   repeat match goal with
   | |- context [ ?F ] =>
     progress match type of F with
-    | FMap _ =>
-       change F with (@fmap _ F);
-       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F)
-    | MBind _ =>
-       change F with (@mbind _ F);
-       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F)
-    | OMap _ =>
-       change F with (@omap _ F);
-       repeat change (@omap _ (@omap _ F)) with (@omap _ F)
+    | FMap' _ _ _ _ =>
+       change F with (@fmap _ _ _ _ F);
+       repeat change (@fmap _ _ _ _ (@fmap _ _ _ _ F)) with (@fmap _ _ _ _ F)
+    | MBind' _ _ _ =>
+       change F with (@mbind _ _ _ F);
+       repeat change (@mbind _ _ _ (@mbind _ _ _ F)) with (@mbind _ _ _ F)
+    | OMap' _ _ _ _ =>
+       change F with (@omap _ _ _ _ F);
+       repeat change (@omap _ _ _ _ (@omap _ _ _ _ F)) with (@omap _ _ _ _ F)
     | Alter _ _ _ =>
        change F with (@alter _ _ _ F);
        repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F)
@@ -313,15 +313,15 @@ Ltac fold_classes_hyps H :=
   repeat match type of H with
   | context [ ?F ] =>
     progress match type of F with
-    | FMap _ =>
-       change F with (@fmap _ F) in H;
-       repeat change (@fmap _ (@fmap _ F)) with (@fmap _ F) in H
-    | MBind _ =>
-       change F with (@mbind _ F) in H;
-       repeat change (@mbind _ (@mbind _ F)) with (@mbind _ F) in H
-    | OMap _ =>
-       change F with (@omap _ F) in H;
-       repeat change (@omap _ (@omap _ F)) with (@omap _ F) in H
+    | FMap' _ _ _ _ =>
+       change F with (@fmap _ _ _ _ F) in H;
+       repeat change (@fmap _ _ _ _ (@fmap _ _ _ _ F)) with (@fmap _ _ _ _ F) in H
+    | MBind' _ _ _ =>
+       change F with (@mbind _ _ _ F) in H;
+       repeat change (@mbind _ _ _ (@mbind _ _ _ F)) with (@mbind _ _ _ F) in H
+    | OMap' _ _ _ _ =>
+       change F with (@omap _ _ _ _ F) in H;
+       repeat change (@omap _ _ _ _ (@omap _ _ _ _ F)) with (@omap _ _ _ _ F) in H
     | Alter _ _ _ =>
        change F with (@alter _ _ _ F) in H;
        repeat change (@alter _ _ _ (@alter _ _ _ F)) with (@alter _ _ _ F) in H
diff --git a/stdpp/telescopes.v b/stdpp/telescopes.v
index ce374c3ec6dd8e540ede99c270e131c85f25c335..d9f88ccfd1ad729672f0ae56a84034f86804877e 100644
--- a/stdpp/telescopes.v
+++ b/stdpp/telescopes.v
@@ -126,7 +126,7 @@ Qed.
 Global Instance tele_fmap {TT : tele} : FMap (tele_fun TT) := λ T U, tele_map.
 
 Lemma tele_fmap_app {T U} {TT : tele} (F : T → U) (t : TT -t> T) (x : TT) :
-  (F <$> t) x = F (t x).
+  tele_app (F <$> t) x = F (t x).
 Proof. apply tele_map_app. Qed.
 
 (** Operate below [tele_fun]s with argument telescope [TT]. *)
diff --git a/tests/universes.v b/tests/universes.v
index a6dcd8d9820dc2cbf9dd52e44796bc984bb03611..4cba3cb5c4f0fd9ee402cae56e1d8e782fbf75d8 100644
--- a/tests/universes.v
+++ b/tests/universes.v
@@ -5,3 +5,7 @@ the types [gmap Z Z] and [gset Z] should have universe [Set] too. *)
 
 Check (gmap Z Z : Set).
 Check (gset Z : Set).
+
+(** Regression test for https://gitlab.mpi-sws.org/iris/stdpp/-/issues/207.
+At least [gmap] should be imported to properly test this. *)
+Definition test A := list (relation A).