fact: Definition from_arrow (a : Arrow) : Term := match a with | Arr f => Morph f end.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify