proposition: Lemma mor_arrow_one_at : forall x y z, inc (R 1) z -> inc y z -> inc x y -> mor (function_cat z) (arrow_one_at x y).
proof: Proof. ir. uf arrow_one_at. ap mor_function_cat_fa_create. am. am. ir. am. Qed.
imports: Arith ordinal nat_trans