proposition: Lemma cocone_transform_vident : forall f c, f = cosocle c -> is_cocone c -> cocone_transform c (vident f) = c.
proof: Proof. ir. uf cocone_transform. rw weak_right_vident. lu. app coedge_nt_axioms. rww source_coedge_nt. Qed.
imports: Arith limits