proposition: Lemma source_cofipr2 : forall a u v, has_cofiprod a u v -> source (cofipr2 a u v) = target v.
proof: Proof. ir. cp (cofiprod_hypothesis_cofiprod H). uh H0; ee. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal