proposition: Lemma is_subcategory_eq : forall a b, is_subcategory a b -> subcategory b (ob a) (mor a) = a.
proof: Proof. ir. assert (lem1 : subcategory_property b (ob a) (mor a)). app is_subcategory_property. cp H. uh H0; ee. ap is_subcategory_extensionality. uhg; ee. app subcategory_axioms. am. rww structure_subcategory. sy; am. ir. rwi ob_subcategory H7; ee. am. am. ir. rwi mor_subcategory H7; ee; am. ir. rwi mor_subcategory H7; rwi mor_subcategory H8; ee. rw comp_subcategory. sy; app H5. am. am. am. am. am. am. am. am. am. ir. rwi ob_subcategory H7; ee. rww id_subcategory. sy; app H6. am. uhg; ee. am. app subcategory_axioms. rww structure_subcategory. ir. rww ob_subcategory; ee; try am. au. ir. rww mor_subcategory; ee; au. ir. rww comp_subcategory. au. au. au. ir. rww id_subcategory. au. au. Qed.
imports: Arith ordinal nat_trans