proposition: Lemma nt2hom_bounded : forall a b, Bounded.axioms (nt2hom a b).
proof: Proof. ir. ap Bounded.criterion. sh (union (Image.create (Cartesian.product (functor_set a b) (functor_set a b)) (fun z => (nt_set (pr1 z) (pr2 z))))). ir. apply union_inc with (nt_set (source y) (target y)). rw inc_nt_set. uh H; ee. uhg; ee. am. tv. tv. rw Image.inc_rw. uh H; ee. sh (pair (source y) (target y)). ee. ap product_pair_inc. rw inc_functor_set. uhg; ee. uh H; ee. am. am. rww target_source. rw inc_functor_set. uhg; ee. uh H; ee; am. rww source_target. am. rw pr1_pair. rw pr2_pair. tv. Qed.
imports: Arith nat_trans