fact: Definition tuple_swap_ab_c_to_a_bc {A B C} (x : A * B * C) : A * (B * C) := match x with ((a, b), c) => (a, (b, c)) end.
imports: Coq.Lists.List Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Applicative Category.Theory.Coq.Monad Category.Theory.Coq.Semigroup Category.Theory.Coq.Monoid