From 7ad02b9716ccbd22edbc6f48e3b2549ff8c0d43a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2016 00:24:21 +0100
Subject: [PATCH] Prove that Fix_F is proper.

---
 prelude/relations.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/prelude/relations.v b/prelude/relations.v
index e5a5436c0..0377f4b4f 100644
--- a/prelude/relations.v
+++ b/prelude/relations.v
@@ -221,3 +221,13 @@ nor by conversion tests in the kernel), but in some cases we do need it for
 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)}
+    (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))
+    (x : A) (acc1 acc2 : Acc R x) :
+  E _ (Fix_F B F acc1) (Fix_F B F acc2).
+Proof. revert x acc1 acc2. fix 2. intros x [acc1] [acc2]; simpl; auto. Qed.
-- 
GitLab