proposition: Lemma cocone_source_cocone_pushdown : forall f c, cocone_source (cocone_pushdown f c) = cocone_source c.
proof: Proof. ir. uf cocone_source. rw cosocle_cocone_pushdown. rw source_fcompose. tv. Qed.
imports: Arith limits