proposition: Theorem Uniform_bij_rule { i : Index } { f : fin_family i -> fin_family i } (f_bij : bijective f) (P : Prop): ⊨ ⦃ P ⦄ (@Uniform_F i) ≈ (@Uniform_F i) ⦃ fun w1 w2 => (f w1) == w2 ⦄.
proof: Proof. eapply (MyRulesU.sample_rule_ch). rewrite Uniform_F_is_uniform_F. apply: (sampleFsq_f_coupling f_bij). by move => a1 a2; apply: sampleFsq_support. Qed.
imports: Coq(RelationClasses Morphisms) 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 RulesProb UniformDistrLemmas choice_type Prelude)