proposition: Theorem ret_ule {A1 A2 : Type} {chA1 : Choice.class_of A1} {chA2 : Choice.class_of A2} (a1 : A1) (a2 : A2) : ⊨ (ord_relmon_unit MFreePr (Choice.Pack chA1) a1) ≈ (ord_relmon_unit MFreePr (Choice.Pack chA2) a2) [{ ret (a1, a2) }].
proof: Proof. rewrite /semantic_judgement /θdex //= /θ0 //=. unfold "≤". simpl. rewrite /MonoCont_order //=. move => π πa1a2. exists (SDistr_unit (F_choice_prod (npair (Choice.Pack chA1) (Choice.Pack chA2))) (a1,a2)). split. - rewrite /SubDistr.SDistr_obligation_1 /=. by apply: SDistr_unit_F_choice_prod_coupling. - move => b1 b2 Hb1b2. by rewrite -(distr_get _ _ Hb1b2). 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)