proposition: Lemma comp_fipr2_fipr_dotted : forall a u v y1 y2, has_fiprod a u v -> fiprod_hypothesis a u v y1 y2 -> comp a (fipr2 a u v) (fipr_dotted a u v y1 y2) = y2.
proof: Proof. ir. cp (cone_compose_fipr_dotted H H0). transitivity (fimap2 (fiprod_cone a u v y1 y2)). wr H1. rw fimap2_cone_compose. rw cone_target_fiprod_cone. rw fimap2_fiprod_cone. tv. ap is_cone_fiprod_cone. app fiprod_hypothesis_fiprod. rww cone_source_fiprod_cone. app cone_composable_fipr_dotted. rww fimap2_fiprod_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal