proposition: Lemma sample_rule : forall {A1 A2} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} (pre : Prop) (post : A1 -> A2 -> Prop) (d1 : SDistr (Choice.Pack chA1)) (d2 : SDistr (Choice.Pack chA2)) d (Hd : coupling d d1 d2) (Hpost : forall a1 a2, d (a1, a2) > 0 -> post a1 a2), ⊨ ⦃ pre ⦄ d1 ≈ d2 ⦃ post ⦄.
proof: Proof. intros. rewrite /semantic_judgement /θ_morph //= /θ0 //=. unfold "≤". simpl. rewrite /MonoCont_order //=. intros pi [H1 H2]. exists d. split. - assumption. - intros a1 a2 Hdp. apply H2. apply Hpost. assumption. Qed.
imports: mathcomp(all_ssreflect all_algebra boolp distr reals realsum) Mon(SpecificationMonads SPropBase SPropMonadicStructures) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd SubDistr Couplings Axioms)