proposition: Lemma is_ob_subcategory : forall a (obp morp:E->Prop) x, is_ob (subcategory a obp morp) x = (is_ob a x & obp x).
proof: Proof. ir. uf subcategory. rw is_ob_create. app iff_eq; ir. ee. Ztac. Ztac. ee. Ztac. Qed.
imports: Arith ordinal nat_trans