fact: Definition lookup_arr (f : nat) dom : option (∃ cod, objD dom ~> objD cod) := let cod := snd (List.nth f tys (0, 0)) in match ith_exact f (dom, cod) arrs with | Some f => Some (cod; f) | _ => None end.
imports: Equations(Equations) Category.Lib Category.Lib.IList Category.Theory.Category Category.Solver.Expr