diff --git a/theories/base.v b/theories/base.v
index d6f95cd4b32c5023fc40ead3223671dc70aa40de..b74ca0552e6049f8f185f98c5f60fcfd0ee6c9e4 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -889,7 +889,8 @@ Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : stdpp_scope.
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
   (at level 100, only parsing, right associativity) : stdpp_scope.
 
-Infix "<$>" := fmap (at level 60, right associativity) : stdpp_scope.
+Infix "<$>" := fmap (at level 61, left associativity) : stdpp_scope.
+
 Notation "' ( x1 , x2 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1, x2) := x in z))
   (at level 100, z at level 200, only parsing, right associativity) : stdpp_scope.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 91af5b33e7f8393a4cf58c88e2f6840912fd1b8b..37a9b4d786cc99f4605acbeb94ecc5a778ad19db 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -628,7 +628,7 @@ Qed.
 Lemma map_fmap_id {A} (m : M A) : id <$> m = m.
 Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
 Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
-  g ∘ f <$> m = g <$> f <$> m.
+  g ∘ f <$> m = g <$> (f <$> m).
 Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
 Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) (m : M A) :
   (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <$> m ≡ f2 <$> m.
diff --git a/theories/finite.v b/theories/finite.v
index a44bfe75385a3f9a890f4b57d4ba8cbdccd08975..b64b94f02dae001540c13c2526000369d1f172cc 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -232,7 +232,7 @@ Section bijective_finite.
 End bijective_finite.
 
 Program Instance option_finite `{Finite A} : Finite (option A) :=
-  {| enum := None :: Some <$> enum A |}.
+  {| enum := None :: (Some <$> enum A) |}.
 Next Obligation.
   constructor.
   - rewrite elem_of_list_fmap. by intros (?&?&?).
@@ -343,7 +343,7 @@ Proof.
 Qed.
 
 Fixpoint fin_enum (n : nat) : list (fin n) :=
-  match n with 0 => [] | S n => 0%fin :: FS <$> fin_enum n end.
+  match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
 Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
 Next Obligation.
   intros n. induction n; simpl; constructor.
diff --git a/theories/list.v b/theories/list.v
index 532224f0fcbd62eabfb00dea9fd1f6b4412504c6..c685c985ba39d9a74876c8574de38870d948d754 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2882,7 +2882,7 @@ Section fmap.
   Context {A B : Type} (f : A → B).
   Implicit Types l : list A.
 
-  Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> f <$> l.
+  Lemma list_fmap_compose {C} (g : B → C) l : g ∘ f <$> l = g <$> (f <$> l).
   Proof. induction l; f_equal/=; auto. Qed.
   Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
     (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
@@ -2898,7 +2898,7 @@ Section fmap.
   Qed.
 
   Definition fmap_nil : f <$> [] = [] := eq_refl.
-  Definition fmap_cons x l : f <$> x :: l = f x :: f <$> l := eq_refl.
+  Definition fmap_cons x l : f <$> x :: l = f x :: (f <$> l) := eq_refl.
 
   Lemma fmap_app l1 l2 : f <$> l1 ++ l2 = (f <$> l1) ++ (f <$> l2).
   Proof. by induction l1; f_equal/=. Qed.
diff --git a/theories/option.v b/theories/option.v
index f149f442e145c91704392cd27d6fb9500b3d4bdb..59b6b7b3cedec48619a72a7dfd83ca3bcd2c4aec 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -202,7 +202,7 @@ Proof. by destruct mx. Qed.
 Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
 Proof. by destruct mx. Qed.
 Lemma option_fmap_compose {A B} (f : A → B) {C} (g : B → C) mx :
-  g ∘ f <$> mx = g <$> f <$> mx.
+  g ∘ f <$> mx = g <$> (f <$> mx).
 Proof. by destruct mx. Qed.
 Lemma option_fmap_ext {A B} (f g : A → B) mx :
   (∀ x, f x = g x) → f <$> mx = g <$> mx.
diff --git a/theories/zmap.v b/theories/zmap.v
index 90c87f5cc094459d3a2e4732700c6ad43d8c8b1a..241b1d3c8bb9ea4b172f7ba0168139ab7d7c3377 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -63,7 +63,7 @@ Proof.
   - intros ??? [??] []; simpl; [done| |]; apply lookup_fmap.
   - intros ? [o t t']; unfold map_to_list; simpl.
     assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
-      prod_map Z.neg id <$> map_to_list t')).
+      (prod_map Z.neg id <$> map_to_list t'))).
     { apply NoDup_app; split_and?.
       - apply (NoDup_fmap_2 _), NoDup_map_to_list.
       - intro. rewrite !elem_of_list_fmap. naive_solver.