fact: Definition mrecursive (f : D ~> itree (D +' E)) : (D +' E) ~> itree E := fun _ m => match m with | inl1 m => mrec f m | inr1 m => ITree.trigger m end.
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)