proposition: Lemma discrete_cat_mor_extens : forall u v, source u = source v -> (exists z, (mor (discrete_cat z) u & mor (discrete_cat z) v)) -> u = v.
proof: Proof. ir. nin H0. ee. rwi mor_discrete_cat3 H0. rwi mor_discrete_cat3 H1. ee. rw H10. rw H5. rw H. reflexivity. Qed.
imports: Arith ordinal nat_trans