proposition: Lemma is_finite_vee_maps : is_finite (vee_maps).
proof: Proof. wr vee_maps_tack. ap finite_tack. ap finite_tack. ap finite_tack. ap finite_tack. ap finite_tack. ap finite_emptyset. Qed.
imports: Arith cat_examples cardinal fc_limits