proposition: Lemma interp_trigger : forall {E F : Type -> Type} {R : Type} (f : E ~> (itree F)) (e : E R), interp f (ITree.trigger e) ≈ f _ e.
proof: Proof. intros; rewrite ITree.Interp.InterpFacts.interp_trigger. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Eq.Shallow) ITree.Core.ITreeDefinition ITree.Basics.Basics ITree.Indexed.Sum ITree.Interp.Interp ITree.Interp.Recursion ITree(Eq.Eqit Eq.UpToTaus Interp.InterpFacts Interp.RecursionFacts)