proposition: Lemma is_finite_vee_cat : is_finite_cat vee_cat.
proof: Proof. uf vee_cat. ap is_finite_catyd. ap vee_data_property. exact (is_finite_vee_obs). exact (is_finite_vee_maps). Qed.
imports: Arith cat_examples cardinal fc_limits