proposition: Lemma θ0_c_sample_vs_s0 (s0 : S) : θ0 c_sample s0 = bindrFree (θ0 c s0) (fun asc => let (a, sc) := asc in bindrFree (θ0 splo sc) (fun rsr => let (r,sr) := rsr in retrFree (a,r,sr))).
proof: Proof. rewrite θ0_vs_c_sample. rewrite /=. rewrite /OrderEnrichedRelativeAdjunctionsExamples.ToTheS_obligation_1. rewrite /FreeProbProg.rFree_obligation_2. reflexivity. 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)