fact: Definition case_ {E F G : Type -> Type} (f : E ~> itree G) (g : F ~> itree G) : E +' F ~> itree G := fun _ ab => match ab with | inl1 a => f _ a | inr1 b => g _ b end.
imports: Coq(Morphisms) ITree(Basics.Basics Basics.Category Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Indexed.Sum Indexed.Relation Interp.Interp Interp.Recursion)