proposition: Lemma cocone_target_cocone_transform : forall u c, cocone_transformable c u -> cocone_target (cocone_transform c u) = cocone_target c.
proof: Proof. ir. uf cocone_target. rww cosocle_cocone_transform. uh H; ee. wr H1. rww target_source. Qed.
imports: Arith limits