proposition: Lemma theta0_vsbind {P Q : ord_choiceType} (p : FrStP S P) (q : FrStP S Q) (s : S) : θ0 (x ∈ P <<- p ;; q) s = (ord_relmon_bind Frp_fld) (fun ps : P * S => let (p,s) := ps in θ0 q s) (θ0 p s).
proof: Proof. unfold θ0. epose (assoc := rlmm_law2 _ _ _ _ (unaryIntState) P Q (fun _ => q) ). cbn in assoc. specialize (assoc p). cbn. unshelve eapply equal_f in assoc. exact s. rewrite [LHS]assoc. unfold OrderEnrichedRelativeAdjunctionsExamples.ToTheS_obligation_1. unfold 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)