proposition: Lemma cocone_source_cocone_transform : forall u c, cocone_transformable c u -> cocone_source (cocone_transform c u) = cocone_source c.
proof: Proof. ir. uf cocone_source. rw cosocle_cocone_transform. uh H; ee. rw source_source. wr source_target. rww H1. am. Qed.
imports: Arith limits