proposition: Lemma socle_fiprod_cone : forall a u v y1 y2, socle (fiprod_cone a u v y1 y2) = vee_functor a u v.
proof: Proof. ir. uf socle. rw edge_nt_fiprod_cone. rw target_vee_nt. tv. Qed.
imports: Arith colimits little_cat fc_limits cardinal