From f27d1cad0a786380142773adabfc4568e668506e 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.

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

diff --git a/prelude/relations.v b/prelude/relations.v
index 0377f4b4f..cf79ffee0 100644
--- a/prelude/relations.v
+++ b/prelude/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