proposition: Lemma ob_twoarrow_cat_or : forall x, ob twoarrow_cat x = (x = (R o1') \/ x = (R o2')).
proof: Proof. ir. ap iff_eq; ir. ufi twoarrow_cat H. rwi ob_catyd H. nin H. nin x0. ap or_introl; am. ap or_intror; am. ap twoarrow_data_property. cp twoarrow_data_property. uf twoarrow_cat. nin H. rw H. app ob_catyd_R. rw H. app ob_catyd_R. Qed.
imports: Arith cat_examples cardinal fc_limits