fact: Definition bimap {E F G H : Type -> Type} (f : E ~> itree G) (g : F ~> itree H) : E +' F ~> itree (G +' H) := case_ (Handler.cat f inl_) (Handler.cat g inr_).
imports: Coq(Morphisms) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Indexed.Sum Indexed.Relation Interp.Interp Interp.Recursion)