proposition: Lemma fa_comp_assoc : forall u v w, inc u (function_arrow_set (source u) (target u)) -> inc v (function_arrow_set (source v) (target v)) -> inc w (function_arrow_set (source w) (target w)) -> source u = target v -> source v = target w -> fa_comp (fa_comp u v) w = fa_comp u (fa_comp v w).
proof: Proof. ir. ap fa_extensionality. ap inc_fas_fa_comp. ap inc_fas_fa_comp. am. am. am. rww source_fa_comp. rww target_fa_comp. am. rww source_fa_comp. rww source_fa_comp. rww target_fa_comp. ap inc_fas_fa_comp. am. ap inc_fas_fa_comp. am. am. am. rw source_fa_comp. tv. rww target_fa_comp. rww target_fa_comp. rww source_fa_comp. rww target_fa_comp. rww source_fa_comp. rww source_fa_comp. rww source_fa_comp. rw target_fa_comp. rww target_fa_comp. rww target_fa_comp. ir. rw V_fa_comp. rw V_fa_comp. rw V_fa_comp. rw V_fa_comp. tv. am. am. am. rwi source_fa_comp H4. am. am. ap inc_fas_fa_comp. am. am. am. rww source_fa_comp. rww target_fa_comp. rww target_fa_comp. rwi source_fa_comp H4. rww source_fa_comp. am. am. am. rwi source_fa_comp H4. ap inc_V_arrow2. am. am. am. ap inc_fas_fa_comp. am. am. am. rww source_fa_comp. rww target_fa_comp. am. rww source_fa_comp. rwi source_fa_comp H4. am. Qed.
imports: Arith ordinal nat_trans