proposition: Lemma ntrans_discrete_nt : forall z a t x, inc x z -> ntrans (discrete_nt z a t) x = (t x).
proof: Proof. ir. uf discrete_nt. rw Nat_Trans.ntrans_create. tv. rw source_discrete_functor. change (is_ob (discrete_cat z) x). ap ob_is_ob. rww ob_discrete_cat. Qed.
imports: Arith ordinal nat_trans