From 4d2f128e355fed111986110b53c46d44f3af7589 Mon Sep 17 00:00:00 2001
From: Simon Friis Vindum <simonfv@gmail.com>
Date: Wed, 22 Apr 2020 15:11:45 +0200
Subject: [PATCH] Combine intro patterns

---
 theories/algebra/agree.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index 84fb02731..e73a3db30 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.
 
-- 
GitLab