proposition: Lemma θ0_vs_c_sample : θ0 c_sample = dnib stT_Frp (fun a : A => dnib stT_Frp (fun r : Arst (op_iota o) => θ0 (retrFree (a, r))) (θ0 splo)) (θ0 c).
proof: Proof. unfold c_sample. rewrite θ0_vs_bind. eapply (f_equal (λ x, dnib stT_Frp x (θ0 c))). apply boolp.funext. move=> a. rewrite θ0_vs_bind. 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)