proposition: Theorem interp_mrec_trigger {U} (a : (D +' E) U) : interp_mrec ctx (ITree.trigger a) ≳ mrecursive ctx _ a.
proof: Proof. rewrite unfold_interp_mrec; unfold mrecursive. destruct a; cbn. rewrite tau_euttge, bind_ret_r. reflexivity. pstep; constructor. intros; left. rewrite tau_euttge, unfold_interp_mrec; cbn. apply reflexivity. Qed.
imports: Paco.paco Coq(Program.Tactics Setoid Morphisms) ITree(Basics.Utils Basics.Category Basics.Basics Basics.Function Core.ITreeDefinition Core.KTree Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Handler Interp.Interp Interp.InterpFacts Interp.Recursion)