proposition: Lemma vcompose_vee_nt : forall a u1 v1 u2 v2 r s t u1' v1' u2' v2' r' s' t', vee_nt_hypothesis a u1 v1 u2 v2 r s t -> vee_nt_hypothesis a u1' v1' u2' v2' r' s' t' -> u1 = u2' -> v1 = v2' -> vcompose (vee_nt a u1 v1 u2 v2 r s t) (vee_nt a u1' v1' u2' v2' r' s' t') = vee_nt a u1' v1' u2 v2 (comp a r r') (comp a s s') (comp a t t').
proof: Proof. ir. wr H1. wr H2. wri H1 H0; wri H2 H0. cp vee_cat_axioms. cp H; cp H0. uh H4; uh H5. ee. assert (vee_hypothesis a u1 v1). uhg; ee; am. assert (vee_hypothesis a u2 v2). uhg; ee; am. assert (vee_hypothesis a u1' v1'). uhg; ee; am. cp (vee_functor_axioms H40). cp (vee_functor_axioms H41). cp (vee_functor_axioms H42). assert (ob a (source u1)). rww ob_source. assert (ob a (target u1)). rww ob_target. assert (ob a (source v1)). rww ob_source. assert (ob a (source u2)). rww ob_source. assert (ob a (target u2)). rww ob_target. assert (ob a (source v2)). rww ob_source. assert (ob a (source u1')). rww ob_source. assert (ob a (target u1')). rww ob_target. assert (ob a (source v1')). rww ob_source. cp (vee_nt_axioms H). cp (vee_nt_axioms H0). assert (source r = target r'). rww H14. assert (source s = target s'). rww H16. assert (source t = target t'). rww H18. assert (vee_nt_hypothesis a u1' v1' u2 v2 (comp a r r') (comp a s s') (comp a t t')). uhg; ee. uh H6; ee; am. am. am. am. am. rww mor_comp. rww mor_comp. rww mor_comp. rww source_comp. rww target_comp. rww source_comp. rww target_comp. rww source_comp. rww target_comp. am. am. rww assoc. rw H21. wrr assoc. rw H38. rww assoc. sy; am. sy; am. rww assoc. rw H22. wrr assoc. rw H39. rww assoc. sy; am. wr H36. am. sy; am. wrr H19. ap Nat_Trans.axioms_extensionality. rw vcompose_axioms. tv. am. am. rw source_vee_nt. rw target_vee_nt. reflexivity. app vee_nt_axioms. rw source_vcompose. rw source_vee_nt. rw source_vee_nt. reflexivity. rw target_vcompose. rw target_vee_nt. rw target_vee_nt. reflexivity. ir. rwi osource_vcompose H61. rwi osource_vee_nt H61. rw ntrans_vcompose. rw otarget_vee_nt. rwi ob_vee_cat_ex H61. nin H61. nin x0. rw H61. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. reflexivity. rw H61. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. reflexivity. rw H61. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. rw ntrans_vee_nt_R. reflexivity. rw osource_vee_nt. am. Qed.
imports: Arith cat_examples cardinal fc_limits