From 4d688329b076d50cf2df4c9192c849eaf483bf79 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2016 09:10:21 +0100
Subject: [PATCH] Simplify Fix_F_proper.

---
 theories/relations.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/relations.v b/theories/relations.v
index cb8ceeea..dfedb109 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -222,9 +222,7 @@ computation (that is, we cannot make it opaque). We use the [Strategy]
 command to make its expanding behavior less eager. *)
 Strategy 100 [wf_guard].
 
-Lemma Fix_F_proper `{R : relation A}
-    (B : A → Type)
-    (E : ∀ x, relation (B x)) {E_Equivalence : ∀ x, Equivalence (E x)}
+Lemma Fix_F_proper `{R : relation A} (B : A → Type) (E : ∀ x, relation (B x))
     (F : ∀ x, (∀ y, R y x → B y) → B x)
     (HF : ∀ (x : A) (f g : ∀ y, R y x → B y),
       (∀ y Hy Hy', E _ (f y Hy) (g y Hy')) → E _ (F x f) (F x g))
-- 
GitLab