proposition: Lemma inc_function_arrow_set : forall a b u, inc u (function_arrow_set a b) = (Arrow.like u & source u = a & target u = b & Function.axioms (arrow u) & Function.domain (arrow u) = a & sub (Function.range (arrow u)) b & Map.axioms a b (arrow u)).
proof: Proof. ir. ap iff_eq; ir. ufi function_arrow_set H. rwi Image.inc_rw H. nin H. dj; ee; cp (function_set_pr H); ee. wr H0. rww Arrow.create_like. wr H1. rww Arrow.source_create. wr H2. rww Arrow.target_create. wr H3. rw Arrow.arrow_create. am. wr H4. rw Arrow.arrow_create. am. wr H5. rw Arrow.arrow_create. uhg; ir. nin (range_ex H7 H10). ee. wr H12. ap H9. wrr H8. uhg; ee. am. am. am. ee. uf function_arrow_set. rw Image.inc_rw. sh (arrow u). ee. ap function_set_inc. am. am. ir. ap H4. ap range_inc. am. sh y. ee; try tv; try am. rww H3. uh H. wr H0. wr H1. sy; am. Qed.
imports: Arith ordinal nat_trans