proposition: Lemma empty_nt_axioms : forall a, Category.axioms a -> Nat_Trans.axioms (empty_nt a).
proof: Proof. ir. uf empty_nt. ap Nat_Trans.create_axioms. uhg; ee. app empty_functor_axioms. app empty_functor_axioms. tv. tv. ir. rwi source_empty_functor H0. rwi ob_empty_cat H0. elim H0. ir. rwi source_empty_functor H0. rwi ob_empty_cat H0. elim H0. ir. rwi source_empty_functor H0. rwi ob_empty_cat H0. elim H0. ir. rwi source_empty_functor H0. rwi mor_empty_cat H0. elim H0. Qed.
imports: Arith ordinal nat_trans