proposition: Lemma fiprod_hypothesis_comp : forall a u v y1 y2 z, fiprod_hypothesis a u v y1 y2 -> mor a z -> source y1 = target z -> fiprod_hypothesis a u v (comp a y1 z) (comp a y2 z).
proof: Proof. ir. uh H; uhg; ee. am. rww mor_comp. rww mor_comp. wrr H6. rww target_comp. rww target_comp. wrr H6. rww source_comp. rww source_comp. wrr H6. wrr assoc. rw H7. rww assoc. uh H; ee. am. wrr H6. uh H; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal