proposition: Lemma ntrans_twoarrow_nt_R : forall a u1 v1 u2 v2 r s (x:obsy twoarrow_data), ntrans (twoarrow_nt a u1 v1 u2 v2 r s) (R x) = match x with o1 => r | o2 => s end.
proof: Proof. ir. uf twoarrow_nt. rw ntrans_nttyd. rw X_rewrite. tv. rw ob_catyd. sh x; tv. ap twoarrow_data_property. Qed.
imports: Arith cat_examples cardinal fc_limits