proposition: Lemma inc_morphism_set_pool : forall r, inc r morphism_set_pool = exists a, exists b, (inc a obs & inc b obs & r = (homs a b)).
proof: Proof. ir. uf morphism_set_pool. rw Image.inc_rw. app iff_eq; ir. nin H; ee. sh (pr1 x). sh (pr2 x). ee; try (sy; am). cp (Cartesian.product_pr H). ee. am. cp (Cartesian.product_pr H). ee. am. nin H. nin H. sh (pair x x0). ee. ap Cartesian.product_pair_inc. am. am. rw pr1_pair. rw pr2_pair. sy; am. Qed.
imports: Arith ordinal nat_trans