proposition: Lemma ntrans_arrow_ev_create : forall f t x, inc x (objects (source f)) -> ntrans_arrow_ev (ntrans_arrow_create f t) x = t x.
proof: Proof. ir. uf ntrans_arrow_ev. uf ntrans_arrow_create. drw. aw. Qed.
imports: Arith functor