proposition: Lemma inc_fa_inclusion_fas : forall a b, sub a b -> inc (fa_inclusion a b) (function_arrow_set a b).
proof: Proof. ir. assert (Map.axioms a b (arrow (fa_inclusion a b))). uhg; ee. rw arrow_fa_inclusion. ap Function.create_axioms. rw arrow_fa_inclusion. rww Function.create_domain. rw arrow_fa_inclusion. uhg; ir. rwi range_inc_rw H0. nin H0. ee. rwi Function.create_domain H0. rwi create_V_rewrite H1. rw H1. ap H. am. am. ap Function.create_axioms. cp H0. uh H1; ee. rw inc_function_arrow_set; xd. uf fa_inclusion. rww Arrow.create_like. rww source_fa_inclusion. rww target_fa_inclusion. Qed.
imports: Arith ordinal nat_trans