proposition: Lemma discrete_nt_property_ntrans : forall z u, Nat_Trans.axioms u -> osource u = discrete_cat z -> discrete_nt_property z (otarget u) (ntrans u).
proof: Proof. ir. uhg; ee. rww category_axioms_otarget. ir. ap mor_ntrans. am. rw H0. rww ob_discrete_cat. tv. Qed.
imports: Arith ordinal nat_trans