proposition: Lemma smMonEqu2 {A1 A2 B : ord_choiceType} {S : choiceType} (r : A1 -> A2 -> FrStP S B) (c1 : FrStP S A1) (c2 : FrStP S A2) : (a1 ∈ choice_incl A1 <<- c1;; a2 ∈ choice_incl A2 <<- c2;; (r a1 a2)) = (a ∈ choice_incl (prod_choiceType A1 A2) <<- (a1 ∈ choice_incl A1 <<- c1;; a2 ∈ choice_incl A2 <<- c2;; retF (a1, a2));; r a.1 a.2).
proof: Proof. symmetry. cbn. unfold FreeProbProg.rFree_obligation_2. unshelve epose (assoc := (@ord_relmon_law3 _ _ _ (FrStP S) _ _ _ _ _)). shelve. shelve. shelve. exact (fun a : A1 * A2 => r a.1 a.2). exact (fun a1 : A1 => bindrFree (@StateTransformingLaxMorph.ops_StP S) (@StateTransformingLaxMorph.ar_StP S) c2 (fun a2 : A2 => retF (a1, a2))). cbn in assoc. unfold FreeProbProg.rFree_obligation_2 in assoc. symmetry in assoc. unshelve eapply equal_f in assoc. exact c1. rewrite assoc. clear assoc. f_equal. apply boolp.funext. move=> a1. unshelve epose (assoc := (@ord_relmon_law3 _ _ _ (FrStP S) _ _ _ _ _)). shelve. shelve. shelve. exact (fun a : A1 * A2 => r a.1 a.2). exact (fun a2 : A2 => retF (a1, a2)). cbn in assoc. unfold FreeProbProg.rFree_obligation_2 in assoc. symmetry in assoc. unshelve eapply equal_f in assoc. exact c2. rewrite assoc. reflexivity. 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)