proposition: Lemma is_id_fun_arrow_id_fc : forall z x, inc x z -> is_id_fun_arrow (id (function_cat z) x).
proof: Proof. ir. uhg; ee. rw id_function_cat. uf fa_id. rw Arrow.source_create. tv. am. Qed.
imports: Arith ordinal nat_trans