proposition: Lemma constant_functor_vee_functor : forall a b x, a = vee_cat -> ob b x -> constant_functor a b x = vee_functor b (id b x) (id b x).
proof: Proof. ir. ap functor_vee_eq2. ap constant_functor_axioms. rw H; ap vee_cat_axioms. uh H0; ee; am. am. rww source_constant_functor. rww target_constant_functor. rw fmor_constant_functor. tv. rw H. ap mor_vee_cat. rw fmor_constant_functor. tv. rw H. ap mor_vee_cat. Qed.
imports: Arith cat_examples cardinal fc_limits