proposition: Lemma is_id_fun_arrow_rw : forall u, is_id_fun_arrow u = (source u = target u & (forall z, inc (source u) z -> (u = (id (function_cat z) (source u))))).
proof: Proof. ir. ap iff_eq; ir. ee. ufi is_id_fun_arrow H. rw H. rw source_fa_id. rww target_fa_id. ir. uh H; ee. rw H. rw source_fa_id. rw id_function_cat. tv. am. uhg; ee. util (H0 (singleton (source u))). ap singleton_inc. rwi id_function_cat H1. am. ap singleton_inc. Qed.
imports: Arith ordinal nat_trans