From 1d45f47442fcb39148ee99bbea37e42f8c354a10 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Sun, 24 Feb 2019 10:46:21 +0100
Subject: [PATCH] Monotonicity for `Acc`.
---
theories/relations.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/relations.v b/theories/relations.v
index ea51a55..8b8a369 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -315,6 +315,10 @@ Section subrel.
End subrel.
(** * Theorems on well founded relations *)
+Lemma Acc_impl {A} (R1 R2 : relation A) x :
+ Acc R1 x → (∀ y1 y2, R2 y1 y2 → R1 y1 y2) → Acc R2 x.
+Proof. induction 1; constructor; naive_solver. Qed.
+
Notation wf := well_founded.
Definition wf_guard `{R : relation A} (n : nat) (wfR : wf R) : wf R :=
Acc_intro_generator n wfR.
--
2.26.2