proposition: Lemma map_eq_complete {X Y : MetricSpace} {plX : PrelengthSpace X} (f g : X --> Y) : (forall x : X, msp_eq (f x) (g x)) -> (forall x : Complete X, msp_eq (Cmap plX f x) (Cmap plX g x)).
proof: Proof. intros A x. apply lift_eq_complete. intro y. rewrite fast_MonadLaw3, fast_MonadLaw3, A. reflexivity. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q