From 625c206136aee406e1d3f7505bd69bfaf84f8e6c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 1 Jun 2016 21:59:36 +0200
Subject: [PATCH] Simplify prod_leibniz.

---
 theories/base.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 6872ec7f..fc03e031 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -466,10 +466,8 @@ Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) :=
 Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
 Typeclasses Opaque prod_equiv.
 
-Instance prod_leibniz `{LeibnizEquiv A, !Equivalence ((≡) : relation A),
-                        LeibnizEquiv B, !Equivalence ((≡) : relation B)}
-  : LeibnizEquiv (A * B).
-Proof. intros [] [] []; fold_leibniz; simpl; congruence. Qed.
+Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
+Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
 
 (** ** Sums *)
 Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' :=
-- 
GitLab