proposition: Theorem post_weaken_rule_ch {A1 A2 : ord_choiceType} {d1 : MFreePr A1} {d2 : MFreePr A2} : forall (pre : Prop) (post1 post2 : A1 -> A2 -> Prop), (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post1 ⦄) -> (forall a1 a2, post1 a1 a2 -> post2 a1 a2) -> (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post2 ⦄).
proof: Proof. move => pre post1 post2 Hjudg Hleq. rewrite /semantic_judgement /θdex //= /θ0 //=. unfold "≤". simpl. rewrite /MonoCont_order //=. move => π H'. apply: Hjudg. simpl; intuition. 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)