proposition: Lemma fob_funtyd : forall d (f:fun_type_data d) x, funtyd_property f -> ob (source (funtyd f)) x -> fob (funtyd f) x = X (fo f) x.
proof: Proof. ir. uf fob. rww fmor_funtyd. rw source_funtyd. rwi source_funtyd H0. cp (R_ob_lift H0). wr H1. rw X_rewrite. uh H; ee. rw id_catyd. rw catyd_id_R. uf funtyd_fmor. rw arrow_catyd_arrow. rw X_rewrite. wr H7. rw source_id. tv. ap H3. rw R_ob_lift. am. rw source_funtyd. ap mor_id. rwi source_funtyd H0; am. Qed.
imports: Arith cat_examples cardinal fc_limits