diff --git a/theories/relations.v b/theories/relations.v
index ea51a550fb7972a44be86168a7e4876c4ed6724c..8b8a3696a8f9b21a28b012eccc5e783d95e0125c 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.