proposition: Lemma inc_umorphism_set : forall a b u, inc u (umorphism_set a b) = (Umorphism.strong_axioms u & source u = a & target u = b).
proof: Proof. ir. ap iff_eq; ir. ufi umorphism_set H. rwi Image.inc_rw H. nin H. ee. wr H0. ap Umorphism.create_strong_axioms. uhg; ee. uhg. ir. cp (function_set_pr H). ee. ap H5. am. wr H0. rww Umorphism.source_create. wr H0. rww Umorphism.target_create. ee. uf umorphism_set. rw Image.inc_rw. sh (arrow u). ee. uh H; ee. ap function_set_inc. uh H2; ee. wr H2. uf Umorphism.create. rw Arrow.arrow_create. ap Function.create_axioms. uh H2. wr H2. uf Umorphism.create. rw Arrow.arrow_create. rw Function.create_domain. rww H0. ir. change (inc (ev u y) (U b)). uh H. uh H; ee. uh H. wr H1. ap H. rww H0. uh H; ee. uh H2. transitivity (Umorphism.create (source u) (target u) (ev u)). ap Umorphism.create_extens. sy; am. sy; am. ir. tv. am. Qed.
imports: Arith ordinal nat_trans