proposition: Lemma inc_fas_fa_id : forall x, inc (fa_id x) (function_arrow_set x x).
proof: Proof. ir. rw inc_function_arrow_set. dj. uf fa_id. rww Arrow.create_like. rww source_fa_id. rww target_fa_id. rw arrow_fa_id. ap Function.identity_axioms. rw arrow_fa_id. rww Function.identity_domain. rw arrow_fa_id. uhg; ir. util (range_ex (f:= Function.identity x) (y:= x0)). ap Function.identity_axioms. am. nin H5. ee. ufi Function.identity H6. rwi create_V_rewrite H6. wrr H6. rwi Function.identity_domain H5. am. rwi Function.identity_domain H5. am. uhg; ee; am. Qed.
imports: Arith ordinal nat_trans