proposition: Lemma eq_fa_create1 : forall a b f u, inc u (function_arrow_set a b) -> (forall x, inc x a -> f x = V x (arrow u)) -> u = fa_create a b f.
proof: Proof. ir. cp H. rwi inc_function_arrow_set H1. ee. ap fa_extensionality. rw H2; rww H3. rw source_fa_create. rw target_fa_create. ap inc_fa_create_fas. uh H7; ee. uhg. ir. rw H0. ap H6. ap range_inc. am. sh x. ee. rww H5. tv. am. rww source_fa_create. rww target_fa_create. ir. rw arrow_fa_create. rw create_V_rewrite. sy; ap H0. wrr H2. wrr H2. Qed.
imports: Arith ordinal nat_trans