proposition: Lemma mor_dotted : forall a, is_cone a -> has_limit (socle a) -> mor (cone_target a) (dotted a).
proof: Proof. ir. uf dotted. app mor_cone_to_limit. app is_limit_limit. rww socle_limit. uf cone_target. rww socle_limit. Qed.
imports: Arith nat_trans