proposition: Lemma interp_trigger {E F : Type -> Type} {R : Type} (f : E ~> (itree F)) (e : E R) : interp f (ITree.trigger e) ≳ f _ e.
proof: Proof. unfold ITree.trigger. rewrite interp_vis. setoid_rewrite interp_ret. setoid_rewrite tau_euttge. rewrite bind_ret_r. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Core.ITreeDefinition Core.KTree Core.KTreeFacts Eq.Shallow Eq.Eqit Eq.UpToTaus Eq.Paco2 Indexed.Sum Indexed.Function Indexed.Relation Interp.Interp Interp.Handler Interp.TranslateFacts)