proposition: Lemma inc_fas_fa_comp : forall a b u v, inc u (function_arrow_set (source u) (target u)) -> inc v (function_arrow_set (source v) (target v)) -> source u = target v -> a = source v -> b = target u -> inc (fa_comp u v) (function_arrow_set a b).
proof: Proof. ir. rw H2; rw H3. clear H2; clear H3. rwi inc_function_arrow_set H. rwi inc_function_arrow_set H0. ee. assert (Map.axioms (source v) (target u) (arrow (fa_comp u v))). rw arrow_fa_comp. apply Map.compose_axioms with (source u). am. rww H1. rw inc_function_arrow_set. ee. uf fa_comp. rww Arrow.create_like. rww source_fa_comp. rww target_fa_comp. uh H14; ee; am. uh H14; ee; am. uh H14; ee; am. am. Qed.
imports: Arith ordinal nat_trans