proposition: Lemma subcategory_is_subcategory : forall a obp morp, subcategory_property a obp morp -> is_subcategory (subcategory a obp morp) a.
proof: Proof. ir. cp H. uh H0; ee. uhg; ee. app subcategory_axioms. am. rww structure_subcategory. ir. rwi ob_subcategory H5. ee; am. am. ir. rwi mor_subcategory H5. ee; am. am. ir. rwi mor_subcategory H5. rwi mor_subcategory H6. ee. rww comp_subcategory. am. am. ir. rwi ob_subcategory H5. ee. rww id_subcategory. am. Qed.
imports: Arith ordinal nat_trans