proposition: Lemma id_twoarrow_cat_R : forall (x:obsy twoarrow_data), id twoarrow_cat (R x) = match x with o1 => (catyd_arrow i1') | o2 => (catyd_arrow i2') end.
proof: Proof. ir. nin x; uf twoarrow_cat; rww id_catyd_R; ap twoarrow_data_property. Qed.
imports: Arith cat_examples cardinal fc_limits