proposition: Lemma mor_fc_arrow_zero_to : forall z x, inc (R 0) z -> inc x z -> mor (function_cat z) (arrow_zero_to x).
proof: Proof. ir. rw mor_function_cat1. ee. uf arrow_zero_to. uf fa_create. rww Arrow.create_like. rww source_arrow_zero_to. rww target_arrow_zero_to. uf arrow_zero_to. rw source_fa_create. rw target_fa_create. ap inc_fa_create_fas. uhg. ir. rwi zero_emptyset H1. nin H1. nin x1. Qed.
imports: Arith ordinal nat_trans