proposition: Theorem pre_hypothesis_rule {A1 A2 : ord_choiceType} {S1 S2 : choiceType} {d1 : FrStP S1 A1} {d2 : FrStP S2 A2} : ∀ (pre : S1 * S2 → Prop) post, (∀ st1 st2, pre (st1, st2) → ⊨ ⦃ (λ st, st.1 = st1 ∧ st.2 = st2 ) ⦄ d1 ≈ d2 ⦃ post ⦄ ) → (⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post ⦄).
proof: Proof. move => pre post Hjudg. move => [st1 st2]. move => π [H1 H2] /=. simpl in π. apply: (Hjudg st1 st2 H1 (st1, st2)). by rewrite /fromPrePost /=. 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)