proposition: Lemma empty_cat_axioms : Category.axioms empty_cat.
proof: Proof. uf empty_cat. ap Category.create_axioms. uhg; ee. ir. ap iff_eq; ir. nin H. elim x0. uh H; ee; am. ir. ap iff_eq; ir. nin H. elim x. uh H; ee; am. ir. nin H. elim x. ir. nin H. elim x. Qed.
imports: Arith ordinal nat_trans