proposition: Lemma rewrite_eqDistrL { A1 A2 : ord_choiceType } {S1 S2 : choiceType } { P } { Q } (c1 c1' : FrStP S1 A1) (c2 : FrStP S2 A2) (H : ⊨ ⦃ P ⦄ c1 ≈ c2 ⦃ Q ⦄) (θeq : forall s : S1, θ_dens (θ0 c1 s) = θ_dens (θ0 c1' s) ) : ⊨ ⦃ P ⦄ c1' ≈ c2 ⦃ Q ⦄.
proof: Proof. move => [s1 s2]. specialize (H (s1, s2)). specialize (θeq s1). rewrite /θ0 /θ_dens /= in θeq. rewrite /θ /= /MonoCont_order /=. rewrite -θeq. by apply H. 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)