fact: Definition judgement_d {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} {c1 : MFreePr (Choice.Pack chA1)} {c2 : MFreePr (Choice.Pack chA2)} {pre : Prop} {post : A1 -> A2 -> Prop} (π : A1 * A2 -> Prop) (Hπ : pre /\ (forall (a1 : A1) (a2 : A2), post a1 a2 -> π (a1, a2))) (J : ⊨ ⦃ pre ⦄ c1 ≈ c2 ⦃ post ⦄) : { d : { distr (F_choice_prod (npair (Choice.Pack chA1) (Choice.Pack chA2))) / R } | coupling d (Theta_dens.unary_theta_dens_obligation_1 (Choice.Pack chA1) c1) (Theta_dens.unary_theta_dens_obligation_1 (Choice.Pack chA2) c2) /\ (forall (a1 : A1) (a2 : A2), 0 < d (a1, a2) -> π (a1, a2)) }.
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)