proposition: Theorem bind_rule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {B1 B2 : Type} {chB1 : Choice.class_of B1} {chB2 : Choice.class_of B2} {f1 : A1 -> MFreePr (Choice.Pack chB1)} {f2 : A2 -> MFreePr (Choice.Pack chB2)} (m1 : MFreePr (Choice.Pack chA1)) (m2 : MFreePr (Choice.Pack chA2)) (wm : WProp (A1 * A2)%type) (judge_wm : ⊨ m1 ≈ m2 [{ wm }]) (wf : (A1 * A2) -> WProp (B1 * B2)%type) (judge_wf : forall a1 a2, ⊨ (f1 a1) ≈ (f2 a2) [{ (wf (a1, a2)) }]) : ⊨ (ord_relmon_bind MFreePr (fun x : (Choice.Pack chA1) => f1 x) m1 ) ≈ (ord_relmon_bind MFreePr (fun x : (Choice.Pack chA2) => f2 x) m2) [{ bind wm wf }].
proof: Proof. rewrite /semantic_judgement //=. eapply (@transitivity _ _ _ _ _). apply (rlmm_law2 _ _ _ _ θdex (⟨ Choice.Pack chA1, Choice.Pack chA2 ⟩) (⟨ Choice.Pack chB1, Choice.Pack chB2 ⟩) ⟨ f1 , f2 ⟩ ⟨ m1 , m2 ⟩). rewrite /semantic_judgement in judge_wm, judge_wf. apply (@omon_bind WProp (A1 * A2) (B1 * B2) _ _ judge_wm). rewrite /pointwise_relation. move=> [a1 a2]. apply (judge_wf a1 a2). Unshelve. cbv. move=> [ff1 Hff1] [ff2 Hff2] [ff3 Hff3]. move=> H21 H32. move=> bPred. move=> H3. apply H21. apply H32. assumption. Qed.
imports: Coq(RelationClasses Morphisms Utf8) Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg RelativeMonadMorph_prod)