proposition: Theorem ret_rule_ch { A1 A2 : ord_choiceType } (a1 : A1) (a2 : A2) : ⊨ pure a1 ≈ pure a2 [{ ret (a1, a2) }].
proof: Proof. destruct A1 as [A1 chA1]. destruct A2 as [A2 chA2]. by apply: ret_rule. 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)