proposition: Lemma osource_vee_nt : forall a u1 v1 u2 v2 r s t, osource (vee_nt a u1 v1 u2 v2 r s t) = vee_cat.
proof: Proof. ir. uf osource. rw source_vee_nt. rww source_vee_functor. Qed.
imports: Arith cat_examples cardinal fc_limits