diff --git a/algebra/auth.v b/algebra/auth.v
index 0e757ac9eb0e058d9c827457c50cfce6d0a5839a..da3d67f85b237d89bef0c6c9220592c0ceb1f4b1 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -155,7 +155,7 @@ Proof.
   - intros [[[?|]|] ?]; rewrite /= ?auth_valid_eq
       ?auth_validN_eq /= ?cmra_included_includedN ?cmra_valid_validN;
       naive_solver eauto using O.
-  - intros n [[[]|] ?] ?; rewrite auth_validN_eq;
+  - intros n [[[]|] ?]; rewrite !auth_validN_eq /=;
       naive_solver eauto using cmra_includedN_S, cmra_validN_S.
   - by split; simpl; rewrite assoc.
   - by split; simpl; rewrite comm.