proposition: Lemma cocone_pushdown_cocone_pushdown : forall f g a, is_cocone a -> Functor.axioms f -> Functor.axioms g -> source g = cocone_target a -> source f = target g -> cocone_pushdown f (cocone_pushdown g a) = cocone_pushdown (fcompose f g) a.
proof: Proof. ir. ap cocone_extensionality. ap is_cocone_cocone_pushdown. ap is_cocone_cocone_pushdown. am. am. am. am. rw cocone_target_cocone_pushdown. am. ap is_cocone_cocone_pushdown. am. ap fcompose_axioms. am. am. am. rw source_fcompose. am. rw vertex_cocone_pushdown. rw vertex_cocone_pushdown. rw vertex_cocone_pushdown. rw fob_fcompose. tv. am. am. am. rw H2. ap ob_vertex. am. rww cosocle_cocone_pushdown. rww cosocle_cocone_pushdown. sy; rw cosocle_cocone_pushdown. rw fcompose_assoc. tv. am. am. app cosocle_axioms. am. am. ir. rwi cocone_source_cocone_pushdown H4. rwi cocone_source_cocone_pushdown H4. rw coedge_cocone_pushdown. rw coedge_cocone_pushdown. rw coedge_cocone_pushdown. rw fmor_fcompose. tv. am. am. am. rw H2. ap mor_coedge. am. am. am. am. am. am. rw cocone_source_cocone_pushdown. am. app is_cocone_cocone_pushdown. Qed.
imports: Arith limits