proposition: Lemma inclusion_cat_sub_trans : forall u v, source u = target v -> (exists z, (mor (inclusion_cat z) u & mor (inclusion_cat z) v)) -> sub (source v) (target u).
proof: Proof. ir. nin H0; ee. rwi mor_inclusion_cat H0. rwi mor_inclusion_cat H1. ee. uh H5; uh H3; ee. apply sub_trans with (source u). rww H. am. Qed.
imports: Arith ordinal nat_trans