proposition: Lemma θ0_OF_c_sample_s0 (s0 : S) : θ0 c_sample s0 = bindrFree (θ0 c s0) (fun asc => let (a, sc) := asc in bindrFree sploP (fun r => retrFree (a,r,sc))).
proof: Proof. rewrite θ0_c_sample_vs_s0. f_equal. apply boolp.funext. move=> [a sc]. rewrite θ0_of_sample. epose (bind_assoc := ord_relmon_law3 Frp_fld _ _ _ _ _). eapply equal_f in bind_assoc. cbn in bind_assoc. rewrite /FreeProbProg.rFree_obligation_2 in bind_assoc. erewrite <- bind_assoc. 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)