proposition: Lemma ucEq_equiv : forall X Y (x y : UniformlyContinuousSpace X Y), ucEq x y <-> msp_eq x y.
proof: Proof. unfold msp_eq, ucEq. split. - intros. split. apply Qle_refl. intros. apply H. - intros. destruct H. apply H0. Qed.
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Metric CoRN.model.structures.QposInf CoRN.stdlib_omissions.List