diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 84fb027315fd1140caae8e1282a710243d7d2e43..e73a3db30b34006a0d79433f3eed4b87406a2d09 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -209,8 +209,7 @@ Qed.
 
 Lemma to_agree_includedN n a b : to_agree a ≼{n} to_agree b ↔ a ≡{n}≡ b.
 Proof.
-  split; last by intros ->.
-  intros (x & Heq). destruct Heq as [_ Hincl].
+  split; last by intros ->. intros [x [_ Hincl]].
   by destruct (Hincl a) as (? & ->%elem_of_list_singleton & ?); first set_solver+.
 Qed.