proposition: Lemma sample_c_is_c_sample (s0 : S): θ_dens (θ0 sample_c s0) = θ_dens (θ0 c_sample s0).
proof: Proof. rewrite (θ_dens_OF_θ0_sample_c_s0 s0). rewrite (θ_dens_OF_θ0_c_sample_s0 s0). unshelve epose (hlp := SD_commutativity' (utheta_dens_fld (Ar o) sploP) (utheta_dens_fld _ (θ0 c s0)) _). shelve. move=> rr /= [aa ss]. exact (SDistr_unit _ (aa,rr,ss)). rewrite hlp. f_equal. apply boolp.funext. move=> [a sc]. 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)