proposition: Lemma eq_discrete_nt : forall z a t u, discrete_nt_property z a t -> Nat_Trans.axioms u -> osource u = discrete_cat z -> otarget u = a -> (forall x, inc x z -> ntrans u x = t x) -> u = discrete_nt z a t.
proof: Proof. ir. ap Nat_Trans.axioms_extensionality. am. app discrete_nt_axioms. rww source_discrete_nt. ap eq_discrete_functor. rww functor_axioms_source. uhg; ee. wr H2. rww category_axioms_otarget. ir. uh H; ee. rww ob_source. au. am. rww target_source. ir. wrr H3. rww source_ntrans. rw H1. rww ob_discrete_cat. rw target_discrete_nt. ap eq_discrete_functor. rww functor_axioms_target. uhg; ee. wr H2. rww category_axioms_otarget. ir. uh H; ee. rww ob_target. au. rww source_target. am. ir. wrr H3. rww target_ntrans. rw H1. rww ob_discrete_cat. ir. rw ntrans_discrete_nt. ap H3. rwi H1 H4. rwi ob_discrete_cat H4; am. rwi H1 H4. rwi ob_discrete_cat H4; am. Qed.
imports: Arith ordinal nat_trans