proposition: Lemma edge_nt_cone_compose : forall c u, edge_nt (cone_compose c u) = (vcompose (edge_nt c) (constant_nt (cone_source c) (cone_target c) u)).
proof: Proof. ir. uf cone_compose. rw edge_nt_cone_create. tv. Qed.
imports: Arith nat_trans