proposition: Lemma θ0_vs_bind {X Y : choiceType} (m : FrStP S X) (k : X -> FrStP S Y): θ0 (bindrFree m k) = (dnib stT_Frp) (fun x:X => θ0 (k x)) (θ0 m).
proof: Proof. assert ( to_dnib : bindrFree m k = (dnib (FrStP S) k) m ). reflexivity. rewrite to_dnib. rewrite /θ0. pose bla := rmm_law2 _ _ _ _ (@unaryIntState S) X Y k. rewrite /= in bla. unshelve eapply equal_f in bla. exact m. rewrite /=. assumption. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(SPropMonadicStructures SpecificationMonads MonadExamples SPropBase FiniteProbabilities) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum finmap.set finmap.finmap xfinmap) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod StateTransformingLaxMorph choice_type)