proposition: Lemma is_cone_cone_pushdown : forall f c, is_cone c -> Functor.axioms f -> source f = cone_target c -> is_cone (cone_pushdown f c).
proof: Proof. ir. uhg; ee. uf cone_pushdown. ap cone_like_cone_create. rw edge_nt_cone_pushdown. app htrans_left_axioms. uh H; ee. am. rw cone_target_cone_pushdown. rw vertex_cone_pushdown. app ob_fob. rw H1. uh H; ee; am. rw edge_nt_cone_pushdown. rw source_htrans_left. rw source_edge_nt. rw fcompose_right_constant_functor. rw cone_source_cone_pushdown. rw cone_target_cone_pushdown. rw vertex_cone_pushdown. tv. am. am. app cone_source_axioms. app ob_vertex. am. Qed.
imports: Arith nat_trans