proposition: Lemma is_fa_inclusion_fa_comp : forall u v, is_fa_inclusion u -> is_fa_inclusion v -> source u = target v -> is_fa_inclusion (fa_comp u v).
proof: Proof. ir. assert (inc (fa_comp u v) (function_arrow_set (source v) (target u))). ap inc_fas_fa_comp. uh H. ee. rw H2. rw source_fa_inclusion. rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. uh H0. ee. rw H2. rw source_fa_inclusion. rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. am. tv. tv. cp H2. rwi inc_function_arrow_set H3. ee. uhg; ee. rw source_fa_comp. rw target_fa_comp. uh H; uh H0; ee. apply sub_trans with (source u). rww H1. am. rw source_fa_comp. rw target_fa_comp. ap fa_extensionality. ap inc_fas_fa_comp. uh H; ee. rw H10. rw source_fa_inclusion; rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. uh H0; ee. rw H10. rw source_fa_inclusion; rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. am. rww source_fa_comp. rww target_fa_comp. rw source_fa_inclusion. rw target_fa_inclusion. ap inc_fa_inclusion_fas. apply sub_trans with (source u). rww H1. uh H0; ee; am. uh H; ee; am. rw source_fa_comp. rww source_fa_inclusion. rw target_fa_comp. rww target_fa_inclusion. ir. rw V_fa_comp. rw arrow_fa_inclusion. rw create_V_rewrite. uh H; uh H0; ee. rw H12; rw H11. rw arrow_fa_inclusion. rw arrow_fa_inclusion. rw create_V_rewrite. rw create_V_rewrite. tv. rwi source_fa_comp H10. tv. rw create_V_rewrite. rwi source_fa_comp H10. rw H1. ap H0; am. rwi source_fa_comp H10. am. rwi source_fa_comp H10. am. uh H; ee. rw H11. rw source_fa_inclusion; rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. uh H0; ee. rw H11. rw source_fa_inclusion; rw target_fa_inclusion. ap inc_fa_inclusion_fas. am. am. rwi source_fa_comp H10. am. Qed.
imports: Arith ordinal nat_trans