proposition: Lemma eq_empty_nt : forall a u, Nat_Trans.axioms u -> osource u = empty_cat -> otarget u = a -> u = empty_nt a.
proof: Proof. ir. assert (Category.axioms a). wr H1. rww category_axioms_otarget. ap Nat_Trans.axioms_extensionality. am. app empty_nt_axioms. rww source_empty_nt. ap eq_empty_functor. rww functor_axioms_source. am. rww target_source. rw target_empty_nt. ap eq_empty_functor. rww functor_axioms_target. rww source_target. am. ir. rwi H0 H3. rwi ob_empty_cat H3. elim H3. Qed.
imports: Arith ordinal nat_trans