proposition: Lemma is_mor_subcategory : forall a (obp morp:E->Prop) u, is_mor (subcategory a obp morp) u = (is_mor a u & morp u).
proof: Proof. ir. uf subcategory. rw is_mor_create. ap iff_eq; ir. ee. Ztac. Ztac. ee. Ztac. Qed.
imports: Arith ordinal nat_trans