proposition: Lemma eq_empty_cat : forall a, Category.axioms a -> structure a = emptyset -> (forall x, ob a x -> False) -> a = empty_cat.
proof: Proof. ir. ap is_subcategory_extensionality. ap show_empty_subcategory. am. ap empty_cat_axioms. am. rww structure_empty_cat. ap show_empty_subcategory. ap empty_cat_axioms. am. ir. rwi ob_empty_cat H2. am. sy; rww structure_empty_cat. Qed.
imports: Arith ordinal nat_trans