proposition: Lemma id_subcategory : forall a obp morp x, subcategory_property a obp morp -> ob a x -> obp x -> id (subcategory a obp morp) x = id a x.
proof: Proof. ir. uf subcategory. rw id_create. tv. Ztac. ap ob_is_ob. am. Qed.
imports: Arith ordinal nat_trans