proposition: Lemma inc_fa_create_fas : forall a b f, Transformation.axioms a b f -> inc (fa_create a b f) (function_arrow_set a b).
proof: Proof. ir. rw inc_function_arrow_set. dj. uf fa_create. rww Arrow.create_like. rww source_fa_create. rww target_fa_create. rw arrow_fa_create. ap Function.create_axioms. rw arrow_fa_create. rww Function.create_domain. uhg; ir. rwi range_inc_rw H5. nin H5. ee. rwi arrow_fa_create H5. rwi Function.create_domain H5. uh H. rwi arrow_fa_create H6. rwi create_V_rewrite H6. rw H6. ap H. am. am. rw arrow_fa_create. ap Function.create_axioms. uhg; ee; am. Qed.
imports: Arith ordinal nat_trans