diff --git a/tests/algebra.v b/tests/algebra.v
index cff006b35fb5dad5262206b75e9b9286d69c142f..d20708c8f85cd4663ffd664ea66e9e58e58a1b85 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -1,4 +1,4 @@
-From iris.algebra Require Import auth excl.
+From iris.algebra Require Import auth excl lib.gmap_view.
 From iris.base_logic.lib Require Import invariants.
 
 (** Make sure that the same [Equivalence] instance is picked for Leibniz OFEs
@@ -48,3 +48,9 @@ Section test_prod.
     Persistent (PROP:=iPropI Σ) (own γ (◯((None, None), Some (to_agree true)))).
   Proof. apply _. Qed.
 End test_prod.
+
+(** Make sure the [auth]/[gmap_view] notation does not mix up its arguments. *)
+Definition auth_check {A : ucmraT} :
+  auth A = authO A := eq_refl.
+Definition gmap_view_check {K : Type} `{Countable K} {V : ofeT} :
+  gmap_view K V = gmap_viewO K V := eq_refl.
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index d94c5caa4a62c0ab44c092528a1604c67b898912..b322f99fcce25f96813b4e76885864e75edba613 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -104,10 +104,6 @@ Definition gmap_viewR (K : Type) `{Countable K} (V : ofeT) : cmraT :=
 Definition gmap_viewUR (K : Type) `{Countable K} (V : ofeT) : ucmraT :=
   viewUR (gmap_view_rel K V).
 
-(** Make sure the notation does not mix up its arguments. *)
-Local Definition gmap_view_check {K : Type} `{Countable K} {V : ofeT} :
-  gmap_view K V = gmap_viewO K V := eq_refl.
-
 Section definitions.
   Context {K : Type} `{Countable K} {V : ofeT}.