proposition: Lemma rewrite_eqDistrL { A1 A2 : ord_choiceType } { P } { Q } (c1 c1' : MFreePr A1) (c2 : MFreePr A2) (H : ⊨ ⦃ P ⦄ c1 ≈ c2 ⦃ Q ⦄) (θeq : θ0 c1 = θ0 c1' ) : ⊨ ⦃ P ⦄ c1' ≈ c2 ⦃ Q ⦄.
proof: Proof. destruct A1 as [A1 chA1]. destruct A2 as [A2 chA2]. rewrite /semantic_judgement /fromPrePost /θdex /=. unfold "≤". rewrite /= /MonoCont_order. rewrite /θ0 /= in θeq. rewrite -θeq. by apply H. 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)