proposition: Lemma twoarrow_nt_axioms : forall a u1 v1 u2 v2 r s, twoarrow_nt_hypothesis a u1 v1 u2 v2 r s -> Nat_Trans.axioms (twoarrow_nt a u1 v1 u2 v2 r s).
proof: Proof. ir. uf twoarrow_nt. ap nttyd_axioms. ap twoarrow_nttyd_property. am. Qed.
imports: Arith cat_examples cardinal fc_limits