proposition: Lemma θ_dens_OF_θ0_c_sample_s0 (s0:S) : θ_dens (θ0 c_sample s0) = SD_bind (utheta_dens_fld _ (θ0 c s0)) (fun asc => let (a,sc) := asc in SD_bind (utheta_dens_fld _ sploP) (fun r => SDistr_unit _ (a,r,sc))).
proof: Proof. rewrite θ0_OF_c_sample_s0. rewrite !/θ_dens. rewrite utheta_dens_vs_bind. unshelve eassert (eq_cont : (λ x : choice_incl (ord_functor_comp (OrderEnrichedRelativeAdjunctionsExamples.unaryTimesS1 S) (OrderEnrichedRelativeAdjunctions.KleisliLeftAdjoint Frp) A), utheta_dens_fld (F_choice_prod_obj ⟨ ord_functor_id ord_choiceType (prod_choiceType A (Arst (op_iota o))), OrderEnrichedRelativeAdjunctionsExamples.mkConstFunc ord_choiceType ord_choiceType S (prod_choiceType A (Arst (op_iota o))) ⟩) (let (a, sc) := x in bindrFree sploP (λ r : choice_incl (Ar o), retrFree (a, r, sc)))) = fun x => let (a,sc) := x in SD_bind (utheta_dens_fld _ sploP) (fun r => SDistr_unit _ (a,r,sc))). apply boolp.funext. move=> [aa ss]. rewrite utheta_dens_vs_bind. reflexivity. rewrite eq_cont. rewrite /=. rewrite !/SD_bind. rewrite /SubDistr.SDistr_obligation_2. rewrite /Theta_dens.unary_theta_dens_obligation_1. 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)