proposition: Lemma reflexivity_rule { A : ord_choiceType } { S : choiceType } (c : FrStP S A): ⊨ ⦃ fun '(s1, s2) => s1 = s2 ⦄ c ≈ c ⦃ eq ⦄.
proof: Proof. move => [st1 st] /=. move => α [H1 H2] /=. subst. exists (coupling_self_SDistr (θ_dens (θ0 c st))). split. - exact: coupling_self. - move => [a1 s1] [a2 s2] H. apply: H2. apply: aux_lemma H. 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)