proposition: Lemma cone_compose_id : forall c, is_cone c -> cone_compose c (id (cone_target c) (vertex c)) = c.
proof: Proof. ir. ap cone_extensionality. rww is_cone_cone_compose. uhg; ee. am. ap mor_id. ap ob_vertex. am. rww target_id. app ob_vertex. am. rww vertex_cone_compose. rww source_id. app ob_vertex. rww socle_cone_compose. ir. rwi cone_source_cone_compose H0. rww edge_cone_compose. rww right_id. app ob_vertex. app mor_edge. rww source_edge. uhg; ee. am. app mor_id. app ob_vertex. rww target_id. app ob_vertex. Qed.
imports: Arith nat_trans