proposition: Lemma fipr_dotted_uni : forall a u v y1 y2 r, has_fiprod a u v -> fiprod_hypothesis a u v y1 y2 -> cone_composable (fiprod_cone a u v (fipr1 a u v) (fipr2 a u v)) r -> cone_compose (fiprod_cone a u v (fipr1 a u v) (fipr2 a u v)) r = fiprod_cone a u v y1 y2 -> fipr_dotted a u v y1 y2 = r.
proof: Proof. ir. uf fipr_dotted. wr H2. rw fiprod_cone_fiprod. ap dotted_unique. ap vee_functor_axioms. uh H0; ee; am. uh H; ee; am. wr fiprod_cone_fiprod. am. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal