proposition: Corollary coupling_eq { A : ord_choiceType } (K1 K2 : MFreePr A ) { Ψ : Prop } (H : ⊨ ⦃ Ψ ⦄ K1 ≈ K2 ⦃ eq ⦄): Ψ -> θ0 K1 = θ0 K2.
proof: Proof. move => Hpsi. apply distr_ext => w. assert (\P_[ θ0 K1 ] (pred1 w) = \P_[ θ0 K2 ] (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(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)