proposition: Lemma ntrans_htrans_left : forall f a x, ob (osource a) x -> ntrans (htrans_left f a) x = fmor f (ntrans a x).
proof: Proof. ir. uf htrans_left. rw ntrans_create. tv. rw source_fcompose. lu. Qed.
imports: Arith functor