fact: Fixpoint from_composition (fs : Composition) : Term := match fs with | Single f => from_arrow f | Composed f gs => Comp (from_arrow f) (from_composition gs) end.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify