proposition: Lemma nttyd_property_ntrans_R : forall d (f g:fun_type_data d) u, Nat_Trans.axioms u -> funtyd_property f -> funtyd_property g -> source u = funtyd f -> target u = funtyd g -> nttyd_property f g (fun (x:obsy d) => ntrans u (R x)).
proof: Proof. ir. assert (lem1 : ft f = otarget u). wr target_source. rw H2. rww target_funtyd. am. assert (lem2 : ft g = otarget u). uf otarget. rw H3. rww target_funtyd. assert (lem3 : osource u = catyd d). uf osource. rw H2. rww source_funtyd. uhg; dj. uh H0; ee; am. am. am. rw lem1; rww lem2. rw lem1. ap mor_ntrans. am. rw lem3. ap ob_catyd_R. am. tv. rw source_ntrans. rw H2. rww fob_funtyd_R. am. rw lem3. ap ob_catyd_R. am. rw target_ntrans. rw H3. rww fob_funtyd_R. am. rw lem3. app ob_catyd_R. rw lem1. wr fmor_funtyd_catyd_arrow. wr fmor_funtyd_catyd_arrow. wr H2; wr H3. wr target_catyd_arrow. wr source_catyd_arrow. app carre. rw lem3. ap mor_catyd_catyd_arrow. am. am. am. Qed.
imports: Arith cat_examples cardinal fc_limits