proposition: Lemma source_edge : forall c x, ob (cone_source c) x -> is_cone c -> source (edge c x) = vertex c.
proof: Proof. ir. uf edge. rw source_ntrans. rw source_edge_nt. rw fob_constant_functor. tv. am. ap ob_vertex. am. am. lu. rww osource_edge_nt. Qed.
imports: Arith nat_trans