proposition: Lemma catyd_comp_catyd_arrow : forall d (u v:morsy d), catyd_comp d (catyd_arrow u) (catyd_arrow v) = catyd_arrow (compy u v).
proof: Proof. ir. uf catyd_comp. rw arrow_catyd_arrow. rw arrow_catyd_arrow. rw X_rewrite. rw X_rewrite. tv. Qed.
imports: Arith cat_examples cardinal fc_limits