proposition: Lemma subcategory_inclusion_trans : forall a b c, is_subcategory a b -> is_subcategory b c -> fcompose (Umorphism.inclusion b c) (Umorphism.inclusion a b) = Umorphism.inclusion a c.
proof: Proof. ir. uf fcompose. uf compose. rw source_inclusion. rw target_inclusion. uf inclusion. assert (sub (U a) (U b)). uhg; ir. uh H; ee. change (is_mor b x). app mor_is_mor. ap H5. app is_mor_mor. assert (sub (U b) (U c)). uhg; ir. uh H0; ee. change (is_mor c x). app mor_is_mor. ap H6. app is_mor_mor. assert (sub (U a) (U c)). apply sub_trans with (U b); try am. app umorphism_create_extensionality. ir. cp (H1 _ H4). cp (H3 _ H4). rww ev_create. rww ev_create. rww ev_create. ir. cp (H1 _ H4). cp (H3 _ H4). rww ev_create. rww ev_create. rww ev_create. Qed.
imports: Arith ordinal nat_trans