proposition: Lemma comp_discrete_cat : forall z u v, mor (discrete_cat z) u -> mor (discrete_cat z) v -> source u = target v -> comp (discrete_cat z) u v = u.
proof: Proof. ir. rwi mor_discrete_cat3 H; rwi mor_discrete_cat3 H0. ee. rw H10. rw H1. rw left_id. wr H3. am. rw ob_discrete_cat. am. rw mor_discrete_cat. ee; am. tv. tv. Qed.
imports: Arith ordinal nat_trans