diff --git a/modures/auth.v b/modures/auth.v
index c821b5de3403683480c144800dda7befa9b2e24f..a860a0b9b9ef63475de6e81c9c0dc51cf893e4f7 100644
--- a/modures/auth.v
+++ b/modures/auth.v
@@ -3,6 +3,7 @@ Local Arguments valid _ _ !_ /.
 Local Arguments validN _ _ _ !_ /.
 
 Record auth (A : Type) : Type := Auth { authoritative : excl A ; own : A }.
+Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
 Arguments own {_} _.
@@ -151,6 +152,12 @@ Arguments authRA : clear implicits.
 (* Functor *)
 Instance auth_fmap : FMap auth := λ A B f x,
   Auth (f <$> authoritative x) (f (own x)).
+Arguments auth_fmap _ _ _ !_ /.
+Lemma auth_fmap_id {A} (x : auth A) : id <$> x = x.
+Proof. by destruct x; rewrite /= excl_fmap_id. Qed.
+Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : auth A) :
+  g ∘ f <$> x = g <$> f <$> x.
+Proof. by destruct x; rewrite /= excl_fmap_compose. Qed.
 Instance auth_fmap_cmra_ne {A B : cmraT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap auth _ A B).
 Proof.
diff --git a/modures/excl.v b/modures/excl.v
index e1a73d31f1ca47c27b2e5c8b3dc898861992bfc3..fdb667dcf84b9ea09b76d2e150f5fac09c83868e 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -156,6 +156,11 @@ Instance excl_fmap : FMap excl := λ A B f x,
   match x with
   | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
   end.
+Lemma excl_fmap_id {A} (x : excl A) : id <$> x = x.
+Proof. by destruct x. Qed.
+Lemma excl_fmap_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
+  g ∘ f <$> x = g <$> f <$> x.
+Proof. by destruct x. Qed.
 Instance excl_fmap_cmra_ne {A B : cofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap excl _ A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.