proposition: Lemma edge_fiprod_cone_R : forall a u v y1 y2 (x:obsy vee_data), edge (fiprod_cone a u v y1 y2) (R x) = match x with o1 => y1 | o2 => (comp a u y1) | o3 => y2 end.
proof: Proof. ir. uf edge. rw edge_nt_fiprod_cone. rw ntrans_vee_nt_R. tv. Qed.
imports: Arith colimits little_cat fc_limits cardinal