proposition: Lemma mor_cone_to_limit : forall a b y, is_cone a -> is_limit b -> socle a = socle b -> y = cone_target b -> mor y (cone_to_limit a b).
proof: Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. uh H3; ee. rw H2; am. Qed.
imports: Arith nat_trans