proposition: Lemma θ0_vs_sample_c : θ0 sample_c = dnib stT_Frp (fun r : Arst (op_iota o) => dnib stT_Frp (fun a : A => θ0 (retrFree (a, r))) (θ0 c)) (θ0 splo).
proof: Proof. unfold sample_c. rewrite θ0_vs_bind. eassert (eqCont : (fun r : Arst (op_iota o) => θ0 (bindrFree c (fun a : choice_incl A => retrFree (a, r)))) = (fun r => _) ). apply boolp.funext. move=> x. rewrite θ0_vs_bind. reflexivity. rewrite eqCont. 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)