proposition: Theorem post_weaken_rule {A1 A2 : ord_choiceType} {S1 S2 : choiceType} {d1 : FrStP S1 A1} {d2 : FrStP S2 A2} : forall (pre : S1 * S2 -> Prop) (post1 post2 : A1 * S1 -> A2 * S2 -> Prop), (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post1 ⦄) -> (forall as1 as2, post1 as1 as2 -> post2 as1 as2) -> (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post2 ⦄).
proof: Proof. move => pre post1 post2 Hjudg Hleq. eapply weaken_rule. - exact Hjudg. - cbv. intuition. 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)