proposition: Theorem bind_rule {A1 A2 B1 B2 : ord_choiceType} {S1 S2 : choiceType} {f1 : A1 → FrStP S1 B1} {f2 : A2 → FrStP S2 B2} (m1 : FrStP S1 A1) (m2 : FrStP S2 A2) (wm : Base.dfst (WrelSt ⟨ A1, A2 ⟩)) (judge_wm : ⊨ m1 ≈ m2 [{ wm }]) (wf : (A1 * A2) → Base.dfst (WrelSt ⟨ B1, B2 ⟩)) (judge_wf : ∀ a1 a2, ⊨ (f1 a1) ≈ (f2 a2) [{ (wf (a1, a2)) }]) : ⊨ (bindF f1 m1 ) ≈ (bindF f2 m2) [{ bindW wm wf }].
proof: Proof. move => [st1 st2]. etransitivity. rewrite /bindF /=. by apply (rlmm_law2 _ _ _ _ θ ⟨ A1, A2 ⟩ ⟨ B1, B2 ⟩ ⟨ f1 , f2 ⟩ ⟨ m1 , m2 ⟩ (st1, st2)). rewrite /semantic_judgement in judge_wm, judge_wf. destruct A1 as [A1 chA1]. destruct A2 as [A2 chA2]. destruct B1 as [B1 chB1]. destruct B2 as [B2 chB2]. simpl in *. apply (@omon_bind WProp (A1 * S1 * (A2 * S2)) (B1 * S1 * (B2 * S2)) _ _ (judge_wm (st1, st2))). move => [[a1 st1'] [a2 st2']]. by apply: (judge_wf a1 a2). 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)