diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 2421f83326bf2b050df89b330ad6a21012ae5bec..306eb8a8d0530d8b80d757067cf8ff96f10b9029 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -121,7 +121,7 @@ Proof.
 Qed.
 Local Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
 Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
-Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
+Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (op (A := agree A)) := ne_proper_2 _.
 
 Lemma agree_included x y : x ≼ y ↔ y ≡ x ⋅ y.
 Proof.