proposition: Lemma vee_nt_ntrans : forall u, Nat_Trans.axioms u -> osource u = vee_cat -> vee_nt (otarget u) (fmor (source u) (catyd_arrow a12')) (fmor (source u) (catyd_arrow a32')) (fmor (target u) (catyd_arrow a12')) (fmor (target u) (catyd_arrow a32')) (ntrans u (R o1')) (ntrans u (R o2')) (ntrans u (R o3')) = u.
proof: Proof. ir. ap Nat_Trans.axioms_extensionality. ap vee_nt_axioms. app vee_nt_hypothesis_ntrans. am. rw source_vee_nt. wr target_source. sy; ap functor_vee_eq. uh H; ee. am. am. am. rw target_vee_nt. uf otarget. sy; ap functor_vee_eq. uh H; ee; am. rww source_target. ir. ufi osource H1. rwi source_vee_nt H1. rwi source_vee_functor H1. rwi ob_vee_cat_ex H1. nin H1. nin x0. rw H1. rw ntrans_vee_nt_R. reflexivity. rw H1. rw ntrans_vee_nt_R. reflexivity. rw H1. rw ntrans_vee_nt_R. reflexivity. Qed.
imports: Arith cat_examples cardinal fc_limits