proposition: Lemma eq_vee_nt : forall u a u1 v1 u2 v2 r s t, Nat_Trans.axioms u -> osource u = vee_cat -> a = (otarget u) -> u1 = (fmor (source u) (catyd_arrow a12')) -> v1 =(fmor (source u) (catyd_arrow a32')) -> u2 =(fmor (target u) (catyd_arrow a12')) -> v2 =(fmor (target u) (catyd_arrow a32')) -> r =(ntrans u (R o1')) -> s =(ntrans u (R o2')) -> t = (ntrans u (R o3')) -> u = vee_nt a u1 v1 u2 v2 r s t.
proof: Proof. ir. rw H1; rw H2; rw H3; rw H4; rw H5; rw H6; rw H7; rw H8; rww vee_nt_ntrans. Qed.
imports: Arith cat_examples cardinal fc_limits