proposition: Lemma vee_nt_axioms : forall a u1 v1 u2 v2 r s t, vee_nt_hypothesis a u1 v1 u2 v2 r s t-> Nat_Trans.axioms (vee_nt a u1 v1 u2 v2 r s t).
proof: Proof. ir. uf vee_nt. ap nttyd_axioms. ap vee_nttyd_property. am. Qed.
imports: Arith cat_examples cardinal fc_limits