proposition: Lemma cone_pushdown_cone_pushdown : forall f g a, is_cone a -> Functor.axioms f -> Functor.axioms g -> source g = cone_target a -> source f = target g -> cone_pushdown f (cone_pushdown g a) = cone_pushdown (fcompose f g) a.
proof: Proof. ir. ap cone_extensionality. ap is_cone_cone_pushdown. ap is_cone_cone_pushdown. am. am. am. am. rw cone_target_cone_pushdown. am. ap is_cone_cone_pushdown. am. ap fcompose_axioms. am. am. am. rw source_fcompose. am. rw vertex_cone_pushdown. rw vertex_cone_pushdown. rw vertex_cone_pushdown. rw fob_fcompose. tv. am. am. am. rw H2. ap ob_vertex. am. rww socle_cone_pushdown. rww socle_cone_pushdown. sy; rw socle_cone_pushdown. rw fcompose_assoc. tv. am. am. app socle_axioms. am. am. ir. rwi cone_source_cone_pushdown H4. rwi cone_source_cone_pushdown H4. rw edge_cone_pushdown. rw edge_cone_pushdown. rw edge_cone_pushdown. rw fmor_fcompose. tv. am. am. am. rw H2. ap mor_edge. am. am. am. am. am. am. rw cone_source_cone_pushdown. am. app is_cone_cone_pushdown. Qed.
imports: Arith nat_trans