proposition: Lemma Cap_weak_correct : forall X Y plX (f:Complete (X --> Y)), msp_eq (Cap_weak plX f) (Cap_weak_slow f).
proof: Proof. intros. split. apply Qle_refl. apply (Cap_fun_correct plX f). 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