proposition: Lemma ob_catyd : forall d x, catyd_property d -> ob (catyd d) x = (exists y:obsy d, x = R y).
proof: Proof. ir. ap iff_eq; ir. uh H0; ee. ufi catyd H1. rwi Category.is_ob_create H1. nin H1. sh x0. sy; am. nin H0. uf ob. ee. app catyd_axioms. uf catyd. rw Category.is_ob_create. rw H0. ap R_inc. Qed.
imports: Arith cat_examples cardinal fc_limits