proposition: Lemma eq_fa_create2 : forall a b f u, (exists z, mor (function_cat z) u) -> source u = a -> target u = b -> (forall x, inc x a -> f x = V x (arrow u)) -> u = fa_create a b f.
proof: Proof. ir. nin H. rwi mor_function_cat3 H; ee. ap eq_fa_create1. wr H0; wrr H1. am. Qed.
imports: Arith ordinal nat_trans