proposition: Lemma target_coedge : forall c x, ob (cocone_source c) x -> is_cocone c -> target (coedge c x) = vertex c.
proof: Proof. ir. uf coedge. rw target_ntrans. rw target_coedge_nt. rw fob_constant_functor. tv. am. ap ob_vertex. am. am. lu. rww osource_coedge_nt. Qed.
imports: Arith limits