diff --git a/theories/base.v b/theories/base.v
index 30ec94664e72c3f15ca1ea9847aa540e88a7c2cd..8e7817bc1cad1a05ecd4ff67f74467ea73a57c1f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -177,21 +177,24 @@ Notation "(≡{ Γ1 , Γ2 , .. , Γ3 } )" := (equivE (pair .. (Γ1, Γ2) .. Γ3)
 with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
 reverse. *)
-Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y ↔ x = y.
-
+Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
+Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (@equiv A _)} (x y : A) :
+  x ≡ y ↔ x = y.
+Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
+ 
 Ltac fold_leibniz := repeat
   match goal with
   | H : context [ @equiv ?A _ _ _ ] |- _ =>
-    setoid_rewrite (leibniz_equiv (A:=A)) in H
+    setoid_rewrite (leibniz_equiv_iff (A:=A)) in H
   | |- context [ @equiv ?A _ _ _ ] =>
-    setoid_rewrite (leibniz_equiv (A:=A))
+    setoid_rewrite (leibniz_equiv_iff (A:=A))
   end.
 Ltac unfold_leibniz := repeat
   match goal with
   | H : context [ @eq ?A _ _ ] |- _ =>
-    setoid_rewrite <-(leibniz_equiv (A:=A)) in H
+    setoid_rewrite <-(leibniz_equiv_iff (A:=A)) in H
   | |- context [ @eq ?A _ _ ] =>
-    setoid_rewrite <-(leibniz_equiv (A:=A))
+    setoid_rewrite <-(leibniz_equiv_iff (A:=A))
   end.
 
 Definition equivL {A} : Equiv A := (=).
diff --git a/theories/co_pset.v b/theories/co_pset.v
index d00c218df74d71f9a95f0ff5b788ee9f83083d46..b0c656325dc507a212841dbcbc55b82052206c33 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -175,7 +175,7 @@ Proof.
 Qed.
 Instance coPset_leibniz : LeibnizEquiv coPset.
 Proof.
-  intros X Y; split; [rewrite elem_of_equiv; intros HXY|by intros ->].
+  intros X Y; rewrite elem_of_equiv; intros HXY.
   apply (sig_eq_pi _), coPset_eq; try apply proj2_sig.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index daaa5c696723f8f5b373cac38b2887465011292f..46646c7dac9c821462f93b1c72e3529b0b327b57 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -162,9 +162,8 @@ Section setoid.
   Qed.    
   Global Instance map_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (M A).
   Proof.
-    intros m1 m2; split.
-    * by intros Hm; apply map_eq; intros i; unfold_leibniz; apply lookup_proper.
-    * by intros <-; intros i; fold_leibniz.
+    intros m1 m2 Hm; apply map_eq; intros i.
+    by unfold_leibniz; apply lookup_proper.
   Qed.
   Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
   Proof.
diff --git a/theories/list.v b/theories/list.v
index 539388af2a80d84596f648fbef5e67aadfec7ab3..84c0b177cb2c9b5f04622c052b64f2ac48dacf7e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -380,10 +380,7 @@ Section setoid.
     by apply cons_equiv, IH.
   Qed.
   Global Instance list_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (list A).
-  Proof.
-    intros l1 l2; split; [|by intros <-].
-    induction 1; f_equal; fold_leibniz; auto.
-  Qed.
+  Proof. induction 1; f_equal; fold_leibniz; auto. Qed.
 End setoid.
 
 Global Instance: Injective2 (=) (=) (=) (@cons A).
diff --git a/theories/option.v b/theories/option.v
index ed262cfb03d0331ea46b8d96d5e8ed121a9d2e22..08bc2bc6b6b84bf78a2f0a3590c4c228f55f761f 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -101,10 +101,7 @@ Section setoids.
   Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A).
   Proof. by constructor. Qed.
   Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
-  Proof.
-    intros x y; split; [destruct 1; fold_leibniz; congruence|].
-    by intros <-; destruct x; constructor; fold_leibniz.
-  Qed.
+  Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed.
   Lemma equiv_None (mx : option A) : mx ≡ None ↔ mx = None.
   Proof. split; [by inversion_clear 1|by intros ->]. Qed.
   Lemma equiv_Some (mx my : option A) x :
diff --git a/theories/orders.v b/theories/orders.v
index 2a8b14243c4205b9093b5f6483ea51de5840c8a5..a8b7f2d20663c0496352813fd2dbbba612c2e995 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -364,7 +364,7 @@ Hint Extern 0 (@Equivalence _ (≡)) =>
 Section partial_order.
   Context `{SubsetEq A, !PartialOrder (@subseteq A _)}.
   Global Instance: LeibnizEquiv A.
-  Proof. split. intros [??]. by apply (anti_symmetric (⊆)). by intros ->. Qed.
+  Proof. intros ?? [??]; by apply (anti_symmetric (⊆)). Qed.
 End partial_order.
 
 (** * Join semi lattices *)