proposition: Lemma inclusion_cat_mor_extens : forall u v, source u = source v -> target u = target v -> (exists z, (mor (inclusion_cat z) u & mor (inclusion_cat z) v)) -> u = v.
proof: Proof. ir. nin H1. ee. rwi mor_inclusion_cat H1. rwi mor_inclusion_cat H2. ee. uh H6; uh H4; ee. rw H8. rw H7. rw H; rw H0. reflexivity. Qed.
imports: Arith ordinal nat_trans