proposition: Theorem Uniform_bij_rule { i j : Index } { S1 S2 : choiceType } { f : fin_family i -> fin_family j } (f_bij : bijective f) (P : S1 * S2 -> Prop) : ⊨ ⦃ P ⦄ (@Uniform_F i S1) ≈ (@Uniform_F j S2) ⦃ fun '(w1, s1) '(w2, s2) => P (s1, s2) /\ (f w1 == w2) ⦄.
proof: Proof. move => [s1 s2] /=. move => π /= [H11 H2]. exists (UniformSQ s1 s2 f_bij). split. - by apply: UniformSQ_f_coupling. - rewrite /UniformSQ. move => [w1 st1] [w2 st2] H. apply: H2. rewrite /UniformFsq_f /= in H. have hfoo1 : (st1 == s1). { destruct (st1 == s1) eqn:Heq; auto. by rewrite Bool.andb_false_l Order.POrderTheory.ltxx in H. } have hfoo2 : (st2 == s2). { destruct (st2 == s2) eqn:Heq; auto. by rewrite Bool.andb_false_r Order.POrderTheory.ltxx in H. } have hfoo3 : (f w1 == w2). { destruct (f w1 == w2) eqn:Heq; auto. by rewrite Bool.andb_false_r Order.POrderTheory.ltxx in H. } move /eqP : hfoo1. move /eqP : hfoo2. move /eqP : hfoo3. move => hfoo3 hfoo2 hfoo1. subst. split; [assumption | by rewrite refl_true ]. Qed.
imports: 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 UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb)