proposition: Lemma ntrans_ple : forall y x, ob c x -> ob a y -> ntrans (ple x) y = edge (pointl y) x.
proof: Proof. ir. uf ple. rww ntrans_create. change (is_ob (source plv) y). rw source_plv. lu. Qed.
imports: Arith colimits functor_cat