proposition: Lemma BindLaw3 : forall X Y Z (a:Complete X) (f:X --> Complete Y) (g:Y-->Complete Z), msp_eq (Cbind_slow g (Cbind_slow f a)) (Cbind_slow (uc_compose (Cbind_slow g) f) a).
proof: Proof. intros X Y Z a f g. change (msp_eq (Cjoin (Cmap_slow_fun g (Cjoin_fun (Cmap_slow f a)))) (Cjoin (Cmap_slow_fun (uc_compose (Cbind_slow g) f) a))). rewrite -> (MonadLaw2 (Cbind_slow g) f). unfold Cbind_slow. rewrite -> (MonadLaw4 g). rewrite -> (MonadLaw2 (Cjoin (X:=Z)) (Cmap_slow g)). symmetry. apply MonadLaw7. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax