fact: Definition case_sum1 {A B C : Type -> Type} (f : A ~> C) (g : B ~> C) : A +' B ~> C := fun _ ab => match ab with | inl1 a => f _ a | inr1 b => g _ b end.
imports: ITree(Basics.Basics Basics.Category Indexed.Relation Indexed.Sum)