proposition: Lemma constant_nt_vee_nt : forall a b u, a = vee_cat -> mor b u -> constant_nt a b u = vee_nt b (id b (source u)) (id b (source u)) (id b (target u)) (id b (target u)) u u u.
proof: Proof. ir. rw H. ap eq_vee_nt. app constant_nt_axioms. ap vee_cat_axioms. uh H0; ee; am. rww osource_constant_nt. rww otarget_constant_nt. rw source_constant_nt. rw fmor_constant_functor. tv. ap mor_vee_cat. rw source_constant_nt. rw fmor_constant_functor. tv. ap mor_vee_cat. rw target_constant_nt. rw fmor_constant_functor. tv. ap mor_vee_cat. rw target_constant_nt. rw fmor_constant_functor. tv. ap mor_vee_cat. rww ntrans_constant_nt. ap ob_vee_cat. rww ntrans_constant_nt. ap ob_vee_cat. rww ntrans_constant_nt. ap ob_vee_cat. Qed.
imports: Arith cat_examples cardinal fc_limits