proposition: Lemma ntrans_nttyd : forall d f g (n : obsy d -> E) x, ob (catyd d) x -> ntrans (nttyd f g n) x = X n x.
proof: Proof. ir. uf nttyd. rw ntrans_create. tv. rw source_funtyd. uh H; ee. am. Qed.
imports: Arith cat_examples cardinal fc_limits