proposition: Lemma θ_dens_vs_bind' {X Y : choiceType} (m : Frp X ) (k : X -> Frp (prod_choiceType Y S)) : θ_dens (bindrFree m k) = (dnib SDistr) (fun xs => θ_dens (k xs)) (utheta_dens_fld _ m).
proof: Proof. assert ( to_dnib : bindrFree m k = (dnib Frp k) m ). reflexivity. rewrite to_dnib. rewrite /θ_dens. pose bla := rmm_law2 _ _ _ _ (@Theta_dens.unary_theta_dens) X (prod_choiceType Y S) 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)