proposition: Lemma mor_function_cat_fa_create : forall z a b f, inc a z -> inc b z -> (forall x, inc x a -> inc (f x) b) -> mor (function_cat z) (fa_create a b f).
proof: Proof. ir. rw mor_function_cat1. ee. uf fa_create; rww Arrow.create_like. rww source_fa_create. rww target_fa_create. rw source_fa_create. rw target_fa_create. app inc_fa_create_fas. Qed.
imports: Arith ordinal nat_trans