proposition: Lemma fob_funtyd_R : forall d (f:fun_type_data d) (x:obsy d), funtyd_property f -> fob (funtyd f) (R x) = fo f x.
proof: Proof. ir. rewrite fob_funtyd. ap X_rewrite. am. rw source_funtyd. ap ob_catyd_R. uh H; ee; am. Qed.
imports: Arith cat_examples cardinal fc_limits