proposition: Lemma id_catyd_R : forall d (x:obsy d), catyd_property d -> id (catyd d) (R x) = catyd_arrow (idy x).
proof: Proof. ir. rw id_catyd. rw catyd_id_R. tv. ap ob_catyd_R. am. Qed.
imports: Arith cat_examples cardinal fc_limits