fact: Definition termD dom cod (e : Term) : option (objD dom ~> objD cod) := match termD_work dom e with | Some (y; f) => match eq_dec y cod with | left H => Some (rew [fun y => _ ~> objD y] H in f) | _ => None end | _ => None end.
imports: Equations(Equations) Category.Lib Category.Lib.IList Category.Theory.Category Category.Solver.Expr