proposition: Theorem ret_rule {A1 A2 : ord_choiceType} {S1 S2 : choiceType} (a1 : A1) (a2 : A2): ⊨ @pure S1 A1 a1 ≈ @pure S2 A2 a2 [{ retW (a1, a2) }].
proof: Proof. rewrite /semantic_judgement /θ. unfold "≤". simpl. rewrite /MonoCont_order //=. move => [ss1 ss2] πa1a2 /=. exists (SDistr_unit (F_choice_prod (npair (prod_choiceType A1 S1) (prod_choiceType A2 S2))) ((a1, ss1), (a2, ss2))). 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(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)