proposition: Lemma BindLaw1 : forall X Y (f:X--> Complete Y) a, msp_eq (Cbind_slow f (Cunit_fun _ a)) (f a).
proof: Proof. intros X Y f a. change (msp_eq (Cjoin (Cmap_slow_fun f (Cunit_fun X a))) (f a)). rewrite -> (MonadLaw3 f a). apply MonadLaw5. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax