proposition: Lemma ntrans_nttyd_R : forall d f g (n : obsy d -> E) (x:obsy d), catyd_property d -> ntrans (nttyd f g n) (R x) = n x.
proof: Proof. ir. rw ntrans_nttyd. rww X_rewrite. app ob_catyd_R. Qed.
imports: Arith cat_examples cardinal fc_limits