proposition: Lemma sample_rule : ∀ {A1 A2} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} (pre : Prop) (post : A1 -> A2 -> Prop) (c1 : MFreePr (Choice.Pack chA1)) (c2 : MFreePr (Choice.Pack chA2)) dc (Hd : coupling dc (get_d c1) (get_d c2)) (Hpost : forall a1 a2, dc (a1, a2) > 0 -> post a1 a2), ⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄.
proof: Proof. move => A1 A2 chA1 chA2 pre post c1 c2 dc Hd Hpost. rewrite /semantic_judgement /θdex //= /θ0 //=. move => pi [H1 H2]. exists dc. split. - apply Hd. - move => a1 a2 Hdp. apply: H2. by apply: Hpost. 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)