From 35340af726b6434285f8888bd49bb02d9e2bf800 Mon Sep 17 00:00:00 2001
From: Calvin Beck <hobbes@ualberta.ca>
Date: Thu, 13 Nov 2025 14:07:07 -0500
Subject: [PATCH] Add refine_trigger lemma.

---
 theories/Interp/FoldCTree.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/Interp/FoldCTree.v b/theories/Interp/FoldCTree.v
index 31b5907..4acf090 100644
--- a/theories/Interp/FoldCTree.v
+++ b/theories/Interp/FoldCTree.v
@@ -226,6 +226,15 @@ Section FoldCTree.
       refine g (Vis e k) ≅ x <- trigger e;; Guard (refine g (k x)).
     Proof. now rewrite unfold_refine. Qed.
 
+    Lemma refine_trigger `{E -< F} (e: E X) :
+        refine g (trigger e : ctree E C X) ~ (trigger e : ctree F D X).
+    Proof.
+      rewrite unfold_refine; cbn.
+      setoid_rewrite sb_guard.
+      setoid_rewrite refine_ret.
+      now rewrite bind_ret_r.
+    Qed.
+
     Lemma refine_guard `{E -< F} (t: ctree E C X) :
       refine g (Guard t) ≅ Guard (refine g t).
     Proof. now rewrite unfold_refine. Qed.