proposition: Lemma θ_dens_OF_θ0_sample_c_s0 (s0:S) : θ_dens (θ0 sample_c s0) = SD_bind (utheta_dens_fld _ sploP) (fun r => SD_bind (utheta_dens_fld _ (θ0 c s0)) (fun asc => let (a,sc) := asc in SDistr_unit _ (a,r,sc))).
proof: Proof. rewrite θ0_OF_sample_c_s0. rewrite !/θ_dens. rewrite utheta_dens_vs_bind. rewrite !/SD_bind. rewrite /=. rewrite /SubDistr.SDistr_obligation_2. f_equal. apply boolp.funext. move=> r. rewrite /Theta_dens.unary_theta_dens_obligation_1. epose (hlp := utheta_dens_vs_bind _ _). rewrite /= in hlp. unfold Theta_dens.unary_theta_dens_obligation_1 in hlp. unfold SubDistr.SDistr_obligation_2 in hlp. erewrite hlp. f_equal. apply boolp.funext. move=> [aa ss]. clear hlp. cbn. f_equal. 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)