proposition: Lemma cone_to_limit_id : forall a b, is_limit a -> a = b -> cone_to_limit a b = id (cone_target b) (vertex b).
proof: Proof. ir. cp H. uh H1; ee. uh H1; ee. ap H3. uhg; ee. am. ap mor_cone_to_limit. am. wr H0; lu. rw H0; tv. rw H0; tv. rw target_cone_to_limit. rw H0; tv. am. wr H0; lu. rw H0; tv. uhg; ee. am. wr H0; ap mor_id. ap ob_vertex. am. rw target_id. rw H0; tv. ap ob_vertex. wr H0; am. wr H0; rw cone_compose_cone_to_limit. rw cone_compose_id. tv. am. am. am. tv. Qed.
imports: Arith nat_trans