fact: Definition iso_inv {a b:Type} (sab : (S * a) + (S * b)) : S * (a + b) := match sab with | inl (s, a) => (s, inl a) | inr (s, b) => (s, inr b) end.
imports: Coq(Setoid Morphisms) ExtLib(Structures.Monad) ITree(Basics.Basics Basics.Category Basics.CategoryKleisli Basics.CategoryKleisliFacts Basics.Monad)