proposition: Lemma inc_catyd_arrow_set : forall d u, inc u (catyd_arrow_set d) = exists v:morsy d, u = catyd_arrow v.
proof: Proof. ir. ap iff_eq; ir. ufi catyd_arrow_set H. cp (IM_exists H). nin H0. sh x; sy; am. uf catyd_arrow_set. ap IM_inc. nin H. sh x; sy; am. Qed.
imports: Arith cat_examples cardinal fc_limits