Combine intro patterns

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.