proposition: Lemma fiprod_vee_nt_hypothesis : forall a u v y1 y2, fiprod_hypothesis a u v y1 y2 -> vee_nt_hypothesis a (id a (source y1)) (id a (source y2)) u v y1 (comp a u y1) y2.
proof: Proof. ir. uh H; ee. uh H; ee. assert (ob a (source y1)). rww ob_source. assert (ob a (target y1)). rww ob_target. assert (ob a (source y2)). rww ob_source. assert (ob a (target y2)). rww ob_target. uhg; ee. uh H; ee; am. app mor_id. app mor_id. am. am. am. rww mor_comp. am. rww source_id. sy; am. rww source_comp. rww target_id. rww target_comp. rww source_id. sy; am. rww H4. am. rww assoc. rww right_id. app mor_id. rww target_id. rww assoc. rww right_id. app mor_id. rww target_id. Qed.
imports: Arith colimits little_cat fc_limits cardinal