proposition: Corollary coupling_eq { A : ord_choiceType } { S : choiceType } (K1 K2 : FrStP S A ) (ψ : S * S -> Prop) (H : ⊨ ⦃ ψ ⦄ K1 ≈ K2 ⦃ eq ⦄): forall s1 s2, ψ (s1, s2) -> θ_dens (θ0 K1 s1) = θ_dens (θ0 K2 s2).
proof: Proof. move => s1 s2 psi_s1_s2. apply distr_ext => /= w. assert (\P_[ θ_dens (θ0 K1 s1) ] (pred1 w) = \P_[ θ_dens (θ0 K2 s2) ] (pred1 w)). { apply: (Pr_eq ψ eq); rewrite //= => x y Heq. by subst. } by repeat rewrite -pr_pred1 in H0. 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)