fact: Definition htrigger {A B} (m : A ~> B) : A ~> itree B := fun _ e => ITree.trigger (m _ e).
imports: Coq(Morphisms) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Indexed.Sum Indexed.Relation Interp.Interp Interp.Recursion)