fact: Definition uc_id (X:MetricSpace) : UniformlyContinuousFunction X X := Build_UniformlyContinuousFunction (uc_id_prf X).
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List