proposition: Theorem bind_rule_pp {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) (pre : S1 * S2 → Prop) (middle : (A1 * S1) → (A2 * S2) → Prop) (post : (B1 * S1) → (B2 * S2) → Prop) (judge_wm : ⊨ ⦃ pre ⦄ m1 ≈ m2 ⦃ middle ⦄) (judge_wf : ∀ a1 a2, ⊨ ⦃ λ '(s1, s2), middle (a1, s1) (a2, s2) ⦄ f1 a1 ≈ f2 a2 ⦃ post ⦄ ) : ⊨ ⦃ pre ⦄ (bindrFree _ _ m1 f1 ) ≈ (bindrFree _ _ m2 f2) ⦃ post ⦄.
proof: Proof. destruct S1, S2, A1, A2, B1, B2. eapply weaken_rule. - apply bind_rule with (wf := (fun '(a1, a2) => fromPrePost (fun '(s1, s2) => middle (a1, s1) (a2, s2)) post)). + exact judge_wm. + exact judge_wf. - cbv. intuition auto with funelim. 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)