proposition: Lemma V_fa_comp : forall u v x, inc u (function_arrow_set (source u) (target u)) -> inc v (function_arrow_set (source v) (target v)) -> source u = target v -> inc x (source v) -> V x (arrow (fa_comp u v)) = V (V x (arrow v)) (arrow u).
proof: Proof. ir. rw arrow_fa_comp. rw compose_ev. tv. assert (inc (fa_comp u v) (function_arrow_set (source v) (target u))). ap inc_fas_fa_comp. am. am. am. tv. tv. rwi inc_function_arrow_set H3. ee. wr arrow_fa_comp. rw H7. am. Qed.
imports: Arith ordinal nat_trans