proposition: Lemma discrete_nt_axioms : forall z a t, discrete_nt_property z a t -> Nat_Trans.axioms (discrete_nt z a t).
proof: Proof. ir. uh H; ee. uf discrete_nt. ap Nat_Trans.create_axioms. uhg; ee. ap discrete_functor_axioms. uhg; ee. am. ir. rw ob_source. tv. au. ap discrete_functor_axioms. uhg; ee. am. ir. rw ob_target. tv. au. rw source_discrete_functor. rww source_discrete_functor. rw target_discrete_functor. rww target_discrete_functor. ir. rwi source_discrete_functor H1. rw target_discrete_functor. ap H0. wrr ob_discrete_cat. ir. rwi source_discrete_functor H1. rw fob_discrete_functor. tv. uhg; ee. am. ir. rww ob_source. ap H0. am. wrr ob_discrete_cat. ir. rwi source_discrete_functor H1. rw fob_discrete_functor. tv. uhg; ee. am. ir. rww ob_target. ap H0. am. wrr ob_discrete_cat. ir. rw target_discrete_functor. rwi source_discrete_functor H1. cp H1. rwi mor_discrete_cat3 H2. ee. rww fmor_discrete_functor. rww fmor_discrete_functor. wr H4. rw left_id. rw right_id. tv. rww ob_source. ap H0. am. app H0. tv. tv. rww ob_target. app H0. app H0. tv. tv. Qed.
imports: Arith ordinal nat_trans