proposition: Lemma source_coedge : forall c x, ob (cocone_source c) x -> is_cocone c -> source (coedge c x) = fob (cosocle c) x.
proof: Proof. ir. uf coedge. rw source_ntrans. tv. uh H0; ee. am. ufi cocone_source H. ufi cosocle H. am. Qed.
imports: Arith limits