proposition: Lemma id_vee_cat_R : forall (x:obsy vee_data), id vee_cat (R x) = match x with o1 => (catyd_arrow i1') | o2 => (catyd_arrow i2') | o3 => (catyd_arrow i3') end.
proof: Proof. ir. nin x; uf vee_cat; rww id_catyd_R; ap vee_data_property. Qed.
imports: Arith cat_examples cardinal fc_limits