proposition: Lemma fmor_funtyd_catyd_arrow : forall d (f:fun_type_data d) (u:morsy d), funtyd_property f -> fmor (funtyd f) (catyd_arrow u) = fm f u.
proof: Proof. ir. rw fmor_funtyd. uf funtyd_fmor. rw arrow_catyd_arrow. rw X_rewrite. tv. rw source_funtyd. ap mor_catyd_catyd_arrow. uh H; ee; am. Qed.
imports: Arith cat_examples cardinal fc_limits